# 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 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left({A}\mathrm{Colinear}⟨{B},{C}⟩↔{A}\mathrm{Colinear}⟨{C},{B}⟩\right)$

### Proof

Step Hyp Ref Expression
1 btwncom ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left({A}\mathrm{Btwn}⟨{B},{C}⟩↔{A}\mathrm{Btwn}⟨{C},{B}⟩\right)$
2 3anrot ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)↔\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)$
3 btwncom ${⊢}\left({N}\in ℕ\wedge \left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\right)\to \left({B}\mathrm{Btwn}⟨{C},{A}⟩↔{B}\mathrm{Btwn}⟨{A},{C}⟩\right)$
4 2 3 sylan2b ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left({B}\mathrm{Btwn}⟨{C},{A}⟩↔{B}\mathrm{Btwn}⟨{A},{C}⟩\right)$
5 3anrot ${⊢}\left({C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)↔\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)$
6 btwncom ${⊢}\left({N}\in ℕ\wedge \left({C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\right)\to \left({C}\mathrm{Btwn}⟨{A},{B}⟩↔{C}\mathrm{Btwn}⟨{B},{A}⟩\right)$
7 5 6 sylan2br ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left({C}\mathrm{Btwn}⟨{A},{B}⟩↔{C}\mathrm{Btwn}⟨{B},{A}⟩\right)$
8 1 4 7 3orbi123d ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({A}\mathrm{Btwn}⟨{B},{C}⟩\vee {B}\mathrm{Btwn}⟨{C},{A}⟩\vee {C}\mathrm{Btwn}⟨{A},{B}⟩\right)↔\left({A}\mathrm{Btwn}⟨{C},{B}⟩\vee {B}\mathrm{Btwn}⟨{A},{C}⟩\vee {C}\mathrm{Btwn}⟨{B},{A}⟩\right)\right)$
9 3orcomb ${⊢}\left({A}\mathrm{Btwn}⟨{C},{B}⟩\vee {B}\mathrm{Btwn}⟨{A},{C}⟩\vee {C}\mathrm{Btwn}⟨{B},{A}⟩\right)↔\left({A}\mathrm{Btwn}⟨{C},{B}⟩\vee {C}\mathrm{Btwn}⟨{B},{A}⟩\vee {B}\mathrm{Btwn}⟨{A},{C}⟩\right)$
10 8 9 syl6bb ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left(\left({A}\mathrm{Btwn}⟨{B},{C}⟩\vee {B}\mathrm{Btwn}⟨{C},{A}⟩\vee {C}\mathrm{Btwn}⟨{A},{B}⟩\right)↔\left({A}\mathrm{Btwn}⟨{C},{B}⟩\vee {C}\mathrm{Btwn}⟨{B},{A}⟩\vee {B}\mathrm{Btwn}⟨{A},{C}⟩\right)\right)$
11 brcolinear ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left({A}\mathrm{Colinear}⟨{B},{C}⟩↔\left({A}\mathrm{Btwn}⟨{B},{C}⟩\vee {B}\mathrm{Btwn}⟨{C},{A}⟩\vee {C}\mathrm{Btwn}⟨{A},{B}⟩\right)\right)$
12 3ancomb ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)↔\left({A}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)$
13 brcolinear ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\right)\to \left({A}\mathrm{Colinear}⟨{C},{B}⟩↔\left({A}\mathrm{Btwn}⟨{C},{B}⟩\vee {C}\mathrm{Btwn}⟨{B},{A}⟩\vee {B}\mathrm{Btwn}⟨{A},{C}⟩\right)\right)$
14 12 13 sylan2b ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left({A}\mathrm{Colinear}⟨{C},{B}⟩↔\left({A}\mathrm{Btwn}⟨{C},{B}⟩\vee {C}\mathrm{Btwn}⟨{B},{A}⟩\vee {B}\mathrm{Btwn}⟨{A},{C}⟩\right)\right)$
15 10 11 14 3bitr4d ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\right)\to \left({A}\mathrm{Colinear}⟨{B},{C}⟩↔{A}\mathrm{Colinear}⟨{C},{B}⟩\right)$