Metamath Proof Explorer

Theorem colinearperm1

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

Ref Expression
Assertion colinearperm1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ A Colinear C B

Proof

Step Hyp Ref Expression
1 btwncom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ↔ A Btwn C B
2 3anrot ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ↔ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N
3 btwncom ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B Btwn C A ↔ B Btwn A C
4 2 3 sylan2b ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Btwn C A ↔ B Btwn A C
5 3anrot ⊢ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ↔ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
6 btwncom ⊢ N ∈ ℕ ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → C Btwn A B ↔ C Btwn B A
7 5 6 sylan2br ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → C Btwn A B ↔ C Btwn B A
8 1 4 7 3orbi123d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ↔ A Btwn C B ∨ B Btwn A C ∨ C Btwn B A
9 3orcomb ⊢ A Btwn C B ∨ B Btwn A C ∨ C Btwn B A ↔ A Btwn C B ∨ C Btwn B A ∨ B Btwn A C
10 8 9 bitrdi ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ↔ A Btwn C B ∨ C Btwn B A ∨ B Btwn A C
11 brcolinear ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
12 3ancomb ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ↔ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
13 brcolinear ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear C B ↔ A Btwn C B ∨ C Btwn B A ∨ B Btwn A C
14 12 13 sylan2b ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear C B ↔ A Btwn C B ∨ C Btwn B A ∨ B Btwn A C
15 10 11 14 3bitr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ A Colinear C B