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