English
If x and y are on the same ray and are nonzero, then there exist positive scalars r1, r2 with r1 x = r2 y.
Русский
Если x и y на одном луче и ненулевые, то существуют положительные скаляры r1, r2 такие, что r1 x = r2 y.
LaTeX
$$exists_pos (h) (hx) (hy) : ∃ r1 r2 > 0, r1 x = r2 y$$
Lean4
/-- `SameRay` is transitive unless the vector in the middle is zero and both other vectors are
nonzero. -/
theorem trans (hxy : SameRay R x y) (hyz : SameRay R y z) (hy : y = 0 → x = 0 ∨ z = 0) : SameRay R x z :=
by
rcases eq_or_ne x 0 with (rfl | hx); · exact zero_left z
rcases eq_or_ne z 0 with (rfl | hz); · exact zero_right x
rcases eq_or_ne y 0 with (rfl | hy)
· exact (hy rfl).elim (fun h => (hx h).elim) fun h => (hz h).elim
rcases hxy.exists_pos hx hy with ⟨r₁, r₂, hr₁, hr₂, h₁⟩
rcases hyz.exists_pos hy hz with ⟨r₃, r₄, hr₃, hr₄, h₂⟩
refine Or.inr (Or.inr <| ⟨r₃ * r₁, r₂ * r₄, mul_pos hr₃ hr₁, mul_pos hr₂ hr₄, ?_⟩)
rw [mul_smul, mul_smul, h₁, ← h₂, smul_comm]
