Metamath Proof Explorer


Theorem colinearperm3

Description: Permutation law for colinearity. Part of theorem 4.11 of Schwabhauser p. 36. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion colinearperm3 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐵 Colinear ⟨ 𝐶 , 𝐴 ⟩ ) )

Proof

Step Hyp Ref Expression
1 3orrot ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
2 1 a1i ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) )
3 brcolinear ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )
4 3anrot ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
5 brcolinear ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Colinear ⟨ 𝐶 , 𝐴 ⟩ ↔ ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) )
6 4 5 sylan2b ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Colinear ⟨ 𝐶 , 𝐴 ⟩ ↔ ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ) )
7 2 3 6 3bitr4d ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐵 Colinear ⟨ 𝐶 , 𝐴 ⟩ ) )