English
Sbtw is equivalent to x ≠ y and z in the image of lineMap x y with Ioi.
Русский
Sbtw эквивалентно x ≠ y и z находится во изображении lineMap x y под Ioi.
LaTeX
$$Sbtw(R,x,y,z) ⇔ x ≠ y ∧ z ∈ lineMap x y '' Ioi(1)$$
Lean4
theorem sbtw_iff_left_ne_and_right_mem_image_Ioi {x y z : P} :
Sbtw R x y z ↔ x ≠ y ∧ z ∈ lineMap x y '' Set.Ioi (1 : R) :=
by
refine ⟨fun h => ⟨h.left_ne, ?_⟩, fun h => ?_⟩
· obtain ⟨r, ⟨hr, rfl⟩⟩ := h.wbtw.right_mem_image_Ici_of_left_ne h.left_ne
rw [Set.mem_Ici] at hr
rcases hr.lt_or_eq with (hrlt | rfl)
· exact Set.mem_image_of_mem _ hrlt
· simp at h
· rcases h with ⟨hne, r, hr, rfl⟩
rw [Set.mem_Ioi] at hr
refine
⟨wbtw_iff_left_eq_or_right_mem_image_Ici.2
(Or.inr (Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hr Set.Ioi_subset_Ici_self))),
hne.symm, ?_⟩
rw [lineMap_apply, ← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub]
nth_rw 1 [← one_smul R (y -ᵥ x)]
rw [← sub_smul, smul_ne_zero_iff, vsub_ne_zero, sub_ne_zero]
exact ⟨hr.ne, hne.symm⟩
