Theorem colinearperm5

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

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

Proof

Step	Hyp	Ref	Expression
1		colinearperm4	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐶 Colinear ⟨ 𝐴 , 𝐵 ⟩ ) )
2		3anrot	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
3		colinearperm1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Colinear ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝐶 Colinear ⟨ 𝐵 , 𝐴 ⟩ ) )
4	2 3	sylan2br	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐶 Colinear ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝐶 Colinear ⟨ 𝐵 , 𝐴 ⟩ ) )
5	1 4	bitrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐶 Colinear ⟨ 𝐵 , 𝐴 ⟩ ) )