Metamath Proof Explorer

Theorem colinearxfr

Description: Transfer law for colinearity. Theorem 4.13 of Schwabhauser p. 37. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion colinearxfr 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( B Colinear <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> E Colinear <. D , F >. ) )

Proof

Step Hyp Ref Expression
1 btwnxfr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> E Btwn <. D , F >. ) )
2 1 expcomd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. -> ( B Btwn <. A , C >. -> E Btwn <. D , F >. ) ) )
3 2 imp 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> ( B Btwn <. A , C >. -> E Btwn <. D , F >. ) )
4 cgr3permute4 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. <-> <. C , <. A , B >. >. Cgr3 <. F , <. D , E >. >. ) )
5 biid 
 |-  ( N e. NN <-> N e. NN )
6 3anrot 
 |-  ( ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) <-> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
7 3anrot 
 |-  ( ( F e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) <-> ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) )
8 btwnxfr 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( A Btwn <. C , B >. /\ <. C , <. A , B >. >. Cgr3 <. F , <. D , E >. >. ) -> D Btwn <. F , E >. ) )
9 5 6 7 8 syl3anbr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( A Btwn <. C , B >. /\ <. C , <. A , B >. >. Cgr3 <. F , <. D , E >. >. ) -> D Btwn <. F , E >. ) )
10 9 expcomd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. C , <. A , B >. >. Cgr3 <. F , <. D , E >. >. -> ( A Btwn <. C , B >. -> D Btwn <. F , E >. ) ) )
11 4 10 sylbid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. -> ( A Btwn <. C , B >. -> D Btwn <. F , E >. ) ) )
12 11 imp 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> ( A Btwn <. C , B >. -> D Btwn <. F , E >. ) )
13 cgr3permute3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. <-> <. B , <. C , A >. >. Cgr3 <. E , <. F , D >. >. ) )
14 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 ) ) )
15 3anrot 
 |-  ( ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) <-> ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
16 btwnxfr 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. B , A >. /\ <. B , <. C , A >. >. Cgr3 <. E , <. F , D >. >. ) -> F Btwn <. E , D >. ) )
17 5 14 15 16 syl3anb 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( C Btwn <. B , A >. /\ <. B , <. C , A >. >. Cgr3 <. E , <. F , D >. >. ) -> F Btwn <. E , D >. ) )
18 17 expcomd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. B , <. C , A >. >. Cgr3 <. E , <. F , D >. >. -> ( C Btwn <. B , A >. -> F Btwn <. E , D >. ) ) )
19 13 18 sylbid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. -> ( C Btwn <. B , A >. -> F Btwn <. E , D >. ) ) )
20 19 imp 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> ( C Btwn <. B , A >. -> F Btwn <. E , D >. ) )
21 3 12 20 3orim123d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> ( ( B Btwn <. A , C >. \/ A Btwn <. C , B >. \/ C Btwn <. B , A >. ) -> ( E Btwn <. D , F >. \/ D Btwn <. F , E >. \/ F Btwn <. E , D >. ) ) )
22 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> N e. NN )
23 simp22 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
24 simp21 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
25 simp23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
26 brcolinear 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Colinear <. A , C >. <-> ( B Btwn <. A , C >. \/ A Btwn <. C , B >. \/ C Btwn <. B , A >. ) ) )
27 22 23 24 25 26 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( B Colinear <. A , C >. <-> ( B Btwn <. A , C >. \/ A Btwn <. C , B >. \/ C Btwn <. B , A >. ) ) )
28 27 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> ( B Colinear <. A , C >. <-> ( B Btwn <. A , C >. \/ A Btwn <. C , B >. \/ C Btwn <. B , A >. ) ) )
29 simp32 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
30 simp31 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
31 simp33 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
32 brcolinear 
 |-  ( ( N e. NN /\ ( E e. ( EE ` N ) /\ D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( E Colinear <. D , F >. <-> ( E Btwn <. D , F >. \/ D Btwn <. F , E >. \/ F Btwn <. E , D >. ) ) )
33 22 29 30 31 32 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( E Colinear <. D , F >. <-> ( E Btwn <. D , F >. \/ D Btwn <. F , E >. \/ F Btwn <. E , D >. ) ) )
34 33 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> ( E Colinear <. D , F >. <-> ( E Btwn <. D , F >. \/ D Btwn <. F , E >. \/ F Btwn <. E , D >. ) ) )
35 21 28 34 3imtr4d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> ( B Colinear <. A , C >. -> E Colinear <. D , F >. ) )
36 35 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. -> ( B Colinear <. A , C >. -> E Colinear <. D , F >. ) ) )
37 36 com23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( B Colinear <. A , C >. -> ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. -> E Colinear <. D , F >. ) ) )
38 37 impd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( B Colinear <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> E Colinear <. D , F >. ) )