English
If there exist Q with Q_z ≠ 0 and certain proportional relations between P and Q hold (X and Y coordinates satisfy specific equalities, and their Y relation matches negY-related constraints), then negDblY(P) = (−dblU(P))^3.
Русский
Если существуют точки Q с Q_z ≠ 0 и выполняются определённые пропорциональные соотношения между P и Q (координаты X, Y удовлетворяют заданным равенствам, и отношение по Y согласуется с ограничениями, связанными с negY), то negDblY(P) = (−dblU(P))^3.
LaTeX
$$$\\text{If } hQz\\!:\\!Q_z\\neq 0,\\; hx:\\!P_x Q_z^2 = Q_x P_z^2,\\; hy:\\!P_y Q_z^3 = Q_y P_z^3,\\; hy': P_y Q_z^3 = W'.\\mathrm{negY}(Q) P_z^3, \\text{ then } W'.\\mathrm{negDblY}(P) = (-W'.\\mathrm{dblU}(P))^3.$$$
Lean4
theorem negDblY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
(hy : P y * Q z ^ 3 = Q y * P z ^ 3) (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) :
W'.negDblY P = (-W'.dblU P) ^ 3 :=
by
rw [negDblY, dblX_of_Y_eq hQz hx hy hy', Y_eq_negY_of_Y_eq hQz hx hy hy']
ring1
