English
In Noetherian NoZeroDivisors setting, if Q is a triple with Q z ≠ 0 and the x- and y-coordinates of P and Q satisfy the indicated cross-relations hx, hy and hy' (linking P to Q via their Y-values), then the Z-coordinate of 2P vanishes: W'.dblZ P = 0.
Русский
В обстановке без нулевых делителей, если Q z ≠ 0 и координаты P и Q удовлетворяют указанным перекрёстным соотношениям hx, hy и hy' (соотношение Y-значений через P и Q), то Z-координата 2P равна нулю: W'.dblZ P = 0.
LaTeX
$$$ [NoZeroDivisors\ R] \; Q(z) \neq 0,\; hx: P_x Q_z = Q_x P_z,\; hy: P_y Q_z = Q_y P_z,\; hy': P_y Q_z = W'.negY Q \cdot P_z \; \Rightarrow \; W'.\mathrm{dblZ} P = 0 $$$
Lean4
theorem dblZ_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z)
(hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W'.negY Q * P z) : W'.dblZ P = 0 := by
rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, zero_pow three_ne_zero, mul_zero]
