Y_ne_negY_of_Y_ne — Mathlib

English

If hy and hx hold with Y-values distinct and negY relations, then P_y ≠ W'.negY P.

Русский

Если гипотезы hy и hx выполняются и Y-координаты не тождественно равны, то P_y не равно negY P.

LaTeX

$$$ P_y \\neq W'.negY P $$$

Lean4

theorem Y_ne_negY_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ Q y * P z) : P y ≠ W'.negY P :=
  by
  have hy' : P y * Q z - W'.negY Q * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne hP hQ hPz hQz hx hy
  contrapose! hy
  linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'

Похожие утверждения