English
For vectors x,y and scalars r1,r2,r3,r4, the sign of the angle between r1 x + r2 y and r3 x + r4 y is the sign of the determinant r1 r4 − r2 r3 times the sign of the angle between x and y.
Русский
Для векторов x,y и скаляров r1,r2,r3,r4 знак угла между r1 x + r2 y и r3 x + r4 y равен знаку определителя r1 r4 − r2 r3, умноженному на знак угла между x и y.
LaTeX
$$$\\forall x,y\\in V,\\ r_1,r_2,r_3,r_4\\in\\mathbb{R},\\ (o.oangle (r_1 x + r_2 y) (r_3 x + r_4 y)).sign = \\operatorname{sign}(r_1 r_4 - r_2 r_3) \\cdot (o.oangle(x,y)).sign$$$
Lean4
/-- The sign of the angle between two linear combinations of two vectors is the sign of the
determinant of the factors in those combinations multiplied by the sign of the angle between the
two vectors. -/
theorem oangle_sign_smul_add_smul_smul_add_smul (x y : V) (r₁ r₂ r₃ r₄ : ℝ) :
(o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign :=
by
by_cases hr₁ : r₁ = 0
·
rw [hr₁, zero_smul, zero_mul, zero_add, zero_sub, Left.sign_neg, oangle_sign_smul_left, add_comm,
oangle_sign_smul_add_smul_right, oangle_rev, Real.Angle.sign_neg, sign_mul, mul_neg, mul_neg, neg_mul, mul_assoc]
·
rw [← o.oangle_sign_smul_add_right (r₁ • x + r₂ • y) (r₃ • x + r₄ • y) (-r₃ / r₁), smul_add, smul_smul, smul_smul,
div_mul_cancel₀ _ hr₁, neg_smul, ← add_assoc, add_comm (-(r₃ • x)), ← sub_eq_add_neg, sub_add_cancel, ← add_smul,
oangle_sign_smul_right, oangle_sign_smul_add_smul_left, ← mul_assoc, ← sign_mul, add_mul, mul_assoc,
mul_comm r₂ r₁, ← mul_assoc, div_mul_cancel₀ _ hr₁, add_comm, neg_mul, ← sub_eq_add_neg, mul_comm r₄, mul_comm r₃]
