English
In a 3-dimensional vector space over a field, if certain dot products vanish, then either cross products of pairs vanish, reflecting a linear dependence structure.
Русский
В трёхмерном пространстве над полем, при условии, что некоторые скалярные произведения равны нулю, либо cross(a,b)=0, либо cross(c,d)=0, что отражает линейную зависимость.
LaTeX
$$$ (a \cdot c = 0) \land (b \cdot c = 0) \land (a \cdot d = 0) \land (b \cdot d = 0) \Rightarrow (\operatorname{crossProduct}(a,b)=0 \\lor\\ crossProduct(c,d)=0) $$$
Lean4
theorem crossProduct_eq_zero_of_dotProduct_eq_zero {a b c d : Fin 3 → K} (hac : a ⬝ᵥ c = 0) (hbc : b ⬝ᵥ c = 0)
(had : a ⬝ᵥ d = 0) (hbd : b ⬝ᵥ d = 0) : crossProduct a b = 0 ∨ crossProduct c d = 0 :=
by
by_contra h
simp_rw [not_or, ← ne_eq, crossProduct_ne_zero_iff_linearIndependent] at h
rw [← Matrix.of_row (![a, b]), ← Matrix.of_row (![c, d])] at h
let A : Matrix (Fin 2) (Fin 3) K := .of ![a, b]
let B : Matrix (Fin 2) (Fin 3) K := .of ![c, d]
have hAB : A * B.transpose = 0 := by
ext i j
fin_cases i <;> fin_cases j <;> assumption
replace hAB := rank_add_rank_le_card_of_mul_eq_zero hAB
rw [rank_transpose, h.1.rank_matrix, h.2.rank_matrix, Fintype.card_fin, Fintype.card_fin] at hAB
contradiction
