English
For any R, V, P with NoZeroSmulDivisors, and any x,y,z ∈ P, the conjunction Wbtw R x y z and Wbtw R y x z holds if and only if x = y.
Русский
Пусть R, V, P удовлетворяют условиям NoZeroSmulDivisors и x,y,z ∈ P. Тогда выполняется равносилость: Wbtw R x y z и Wbtw R y x z вместе ⇔ x = y.
LaTeX
$$$$ \\forall R\\, V\\, P\\, x,y,z \\in P,\\ Wbtw\\ R\\ x\\ y\\ z \\land Wbtw\\ R\\ y\\ x\\ z \\iff x = y. $$$$
Lean4
theorem wbtw_swap_left_iff [NoZeroSMulDivisors R V] {x y : P} (z : P) : Wbtw R x y z ∧ Wbtw R y x z ↔ x = y :=
by
constructor
· rintro ⟨hxyz, hyxz⟩
rcases hxyz with ⟨ty, hty, rfl⟩
rcases hyxz with ⟨tx, htx, hx⟩
rw [lineMap_apply, lineMap_apply, ← add_vadd] at hx
rw [← @vsub_eq_zero_iff_eq V, vadd_vsub, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul, ← sub_smul, ← add_smul,
smul_eq_zero] at hx
rcases hx with (h | h)
· nth_rw 1 [← mul_one tx] at h
rw [← mul_sub, add_eq_zero_iff_neg_eq] at h
have h' : ty = 0 := by
refine le_antisymm ?_ hty.1
rw [← h, Left.neg_nonpos_iff]
exact mul_nonneg htx.1 (sub_nonneg.2 hty.2)
simp [h']
· rw [vsub_eq_zero_iff_eq] at h
rw [h, lineMap_same_apply]
· rintro rfl
exact ⟨wbtw_self_left _ _ _, wbtw_self_left _ _ _⟩
