dblXYZ_of_Y_eq — Mathlib

English

When P and Q lie on W and share the same affine Y relation, the vector dblXYZ equals the scalar W.dblU(P) times the standard basis [0,1,0].

Русский

Если P и Q лежат на W и совпадают аффинные условия по Y, то dblXYZ(P) равен dblU(P) умноженному на [0,1,0].

LaTeX

$$$W'.dblXYZ(P) = W'.dblU(P) \cdot \begin{bmatrix}0\\1\\0\end{bmatrix}$$$

Lean4

theorem dblXYZ_of_Y_eq {P Q : Fin 3 → F} (hP : W.Equation P) (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) (hy' : P y * Q z = W.negY Q * P z) :
    W.dblXYZ P = W.dblU P • ![0, 1, 0] := by
  erw [dblXYZ, dblX_of_Y_eq hP hPz hQz hx hy hy', dblY_of_Y_eq hP hPz hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy',
    smul_fin3, mul_zero, mul_one]

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