Metamath Proof Explorer

Theorem btwncomim

Description: Betweenness commutes. Implication version. Theorem 3.2 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwncomim 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Btwn <. B , C >. -> A Btwn <. C , B >. ) )

Proof

Step Hyp Ref Expression
1 btwntriv2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> C Btwn <. A , C >. )
2 1 3adant3r2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> C Btwn <. A , C >. )
3 simpl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> N e. NN )
4 simpr2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
5 simpr1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
6 simpr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
7 axpasch 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. /\ C Btwn <. A , C >. ) -> E. x e. ( EE ` N ) ( x Btwn <. A , A >. /\ x Btwn <. C , B >. ) ) )
8 3 4 5 6 5 6 7 syl132anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. /\ C Btwn <. A , C >. ) -> E. x e. ( EE ` N ) ( x Btwn <. A , A >. /\ x Btwn <. C , B >. ) ) )
9 2 8 mpan2d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Btwn <. B , C >. -> E. x e. ( EE ` N ) ( x Btwn <. A , A >. /\ x Btwn <. C , B >. ) ) )
10 simpll 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
11 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
12 simplr1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
13 axbtwnid 
 |-  ( ( N e. NN /\ x e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( x Btwn <. A , A >. -> x = A ) )
14 10 11 12 13 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. A , A >. -> x = A ) )
15 breq1 
 |-  ( x = A -> ( x Btwn <. C , B >. <-> A Btwn <. C , B >. ) )
16 15 biimpd 
 |-  ( x = A -> ( x Btwn <. C , B >. -> A Btwn <. C , B >. ) )
17 14 16 syl6 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. A , A >. -> ( x Btwn <. C , B >. -> A Btwn <. C , B >. ) ) )
18 17 impd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( x Btwn <. A , A >. /\ x Btwn <. C , B >. ) -> A Btwn <. C , B >. ) )
19 18 rexlimdva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) ( x Btwn <. A , A >. /\ x Btwn <. C , B >. ) -> A Btwn <. C , B >. ) )
20 9 19 syld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Btwn <. B , C >. -> A Btwn <. C , B >. ) )