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 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> B Colinear <. C , A >. ) )

Proof

Step Hyp Ref Expression
1 3orrot 
 |-  ( ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) <-> ( B Btwn <. C , A >. \/ C Btwn <. A , B >. \/ A Btwn <. B , C >. ) )
2 1 a1i 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) <-> ( B Btwn <. C , A >. \/ C Btwn <. A , B >. \/ A Btwn <. B , C >. ) ) )
3 brcolinear 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )
4 3anrot 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) <-> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) )
5 brcolinear 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( B Colinear <. C , A >. <-> ( B Btwn <. C , A >. \/ C Btwn <. A , B >. \/ A Btwn <. B , C >. ) ) )
6 4 5 sylan2b 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Colinear <. C , A >. <-> ( B Btwn <. C , A >. \/ C Btwn <. A , B >. \/ A Btwn <. B , C >. ) ) )
7 2 3 6 3bitr4d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> B Colinear <. C , A >. ) )