English
The sine of the angle between x and y, scaled by the norm of x, equals the sine of the angle between y and x−y scaled by the norm of x−y.
Русский
Синус угла между x и y, умноженный на норму x, равен синусу угла между y и (x−y), умноженному на норму (x−y).
LaTeX
$$$\sin(\angle x,y)\,\|x\| = \sin(\angle y,(x-y))\,\|x-y\|$$$
Lean4
/-- **Law of sines** (sine rule), vector angle form. -/
theorem sin_angle_mul_norm_eq_sin_angle_mul_norm (x y : V) :
Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖ :=
by
obtain rfl | hy := eq_or_ne y 0
· simp
obtain rfl | hx := eq_or_ne x 0
· simp [angle_neg_right, angle_self hy]
obtain rfl | hxy := eq_or_ne x y
· simp [angle_self hx]
have h_sin (x y : V) (hx : x ≠ 0) (hy : y ≠ 0) :
Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) := by
simp [field, mul_assoc, sin_angle_mul_norm_mul_norm]
rw [h_sin x y hx hy, h_sin y (x - y) hy (sub_ne_zero_of_ne hxy)]
have hsub : x - y ≠ 0 := sub_ne_zero_of_ne hxy
simp [field, inner_sub_left, inner_sub_right, real_inner_comm x y]
ring_nf
