English
Under the curve equations and a cross-condition hx = P_x Q_z = Q_x P_z, a certain product involving (P_y Q_z - Q_y P_z) and (P_y Q_z - negY Q P_z) multiplied by P_z Q_z vanishes.
Русский
При уравнениях кривой и перекрёстном условии hx = P_x Q_z = Q_x P_z, заданное произведение (P_y Q_z - Q_y P_z)(P_y Q_z - negY Q P_z) умноженное на P_z Q_z обращается в ноль.
LaTeX
$$$ P_z Q_z\\,(P_y Q_z - Q_y P_z)\\,(P_y Q_z - W'.negY Q P_z) = 0 $$$
Lean4
theorem Y_sub_Y_mul_Y_sub_negY {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
(hx : P x * Q z = Q x * P z) : P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - W'.negY Q * P z) = 0 := by
linear_combination (norm := (rw [negY]; ring1))
Q z ^ 3 * (equation_iff P).mp hP - P z ^ 3 * (equation_iff Q).mp hQ +
(P x ^ 2 * Q z ^ 2 + P x * Q x * P z * Q z + Q x ^ 2 * P z ^ 2 - W'.a₁ * P y * P z * Q z ^ 2 +
W'.a₂ * P x * Q z ^ 2 * P z +
W'.a₂ * Q x * P z ^ 2 * Q z +
W'.a₄ * P z ^ 2 * Q z ^ 2) *
hx
