Metamath Proof Explorer

Theorem btwnxfr

Description: A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of Schwabhauser p. 36. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion 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 >. ) )

Proof

Step Hyp Ref Expression
1 brcgr3 
 |-  ( ( 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 , B >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) ) )
2 simp2 
 |-  ( ( <. A , B >. Cgr <. D , E >. /\ <. A , C >. Cgr <. D , F >. /\ <. B , C >. Cgr <. E , F >. ) -> <. A , C >. Cgr <. D , F >. )
3 1 2 biimtrdi 
 |-  ( ( 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 , C >. Cgr <. D , F >. ) )
4 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 )
5 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 ) )
6 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 ) )
7 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 ) )
8 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 ) )
9 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 ) )
10 cgrxfr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. D , F >. ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )
11 4 5 6 7 8 9 10 syl132anc 
 |-  ( ( 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 , C >. Cgr <. D , F >. ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )
12 3 11 sylan2d 
 |-  ( ( 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. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) )
13 12 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 ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) ) -> E. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) )
14 simprrl 
 |-  ( ( ( ( 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 ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) ) -> e Btwn <. D , F >. )
15 14 14 jca 
 |-  ( ( ( ( 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 ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) ) -> ( e Btwn <. D , F >. /\ e Btwn <. D , F >. ) )
16 simpl1 
 |-  ( ( ( 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 ) ) -> N e. NN )
17 simpl31 
 |-  ( ( ( 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 ) ) -> D e. ( EE ` N ) )
18 simpl33 
 |-  ( ( ( 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 ) ) -> F e. ( EE ` N ) )
19 16 17 18 cgrrflxd 
 |-  ( ( ( 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 ) ) -> <. D , F >. Cgr <. D , F >. )
20 simpr 
 |-  ( ( ( 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 ) ) -> e e. ( EE ` N ) )
21 16 20 18 cgrrflxd 
 |-  ( ( ( 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 ) ) -> <. e , F >. Cgr <. e , F >. )
22 19 21 jca 
 |-  ( ( ( 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 ) ) -> ( <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. e , F >. ) )
23 22 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 ) ) ) /\ e e. ( EE ` N ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) ) -> ( <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. e , F >. ) )
24 simpr 
 |-  ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. )
25 simpr 
 |-  ( ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) -> <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. )
26 simpl2 
 |-  ( ( ( 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 ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
27 simpl3 
 |-  ( ( ( 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 ) ) -> ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) )
28 17 20 18 3jca 
 |-  ( ( ( 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 ) ) -> ( D e. ( EE ` N ) /\ e e. ( EE ` N ) /\ F e. ( EE ` N ) ) )
29 cgr3tr4 
 |-  ( ( 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 ) /\ e e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) ) -> ( ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) -> <. D , <. E , F >. >. Cgr3 <. D , <. e , F >. >. ) )
30 16 26 27 28 29 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 e. ( EE ` N ) ) -> ( ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) -> <. D , <. E , F >. >. Cgr3 <. D , <. e , F >. >. ) )
31 cgr3com 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ e e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. D , <. E , F >. >. Cgr3 <. D , <. e , F >. >. <-> <. D , <. e , F >. >. Cgr3 <. D , <. E , F >. >. ) )
32 16 27 17 20 18 31 syl113anc 
 |-  ( ( ( 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 ) ) -> ( <. D , <. E , F >. >. Cgr3 <. D , <. e , F >. >. <-> <. D , <. e , F >. >. Cgr3 <. D , <. E , F >. >. ) )
33 simpl32 
 |-  ( ( ( 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 ) ) -> E e. ( EE ` N ) )
34 brcgr3 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ e e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. D , <. e , F >. >. Cgr3 <. D , <. E , F >. >. <-> ( <. D , e >. Cgr <. D , E >. /\ <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. E , F >. ) ) )
35 16 17 20 18 17 33 18 34 syl133anc 
 |-  ( ( ( 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 ) ) -> ( <. D , <. e , F >. >. Cgr3 <. D , <. E , F >. >. <-> ( <. D , e >. Cgr <. D , E >. /\ <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. E , F >. ) ) )
36 simpr1 
 |-  ( ( ( ( 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 ) ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. E , F >. ) ) -> <. D , e >. Cgr <. D , E >. )
37 simpr3 
 |-  ( ( ( ( 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 ) ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. E , F >. ) ) -> <. e , F >. Cgr <. E , F >. )
38 16 20 18 33 18 37 cgrcomlrand 
 |-  ( ( ( ( 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 ) ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. E , F >. ) ) -> <. F , e >. Cgr <. F , E >. )
39 36 38 jca 
 |-  ( ( ( ( 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 ) ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. E , F >. ) ) -> ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) )
40 39 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 ) ) ) /\ e e. ( EE ` N ) ) -> ( ( <. D , e >. Cgr <. D , E >. /\ <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. E , F >. ) -> ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) )
41 35 40 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 ) ) ) /\ e e. ( EE ` N ) ) -> ( <. D , <. e , F >. >. Cgr3 <. D , <. E , F >. >. -> ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) )
42 32 41 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 ) ) ) /\ e e. ( EE ` N ) ) -> ( <. D , <. E , F >. >. Cgr3 <. D , <. e , F >. >. -> ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) )
43 30 42 syld 
 |-  ( ( ( 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 ) ) -> ( ( <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) -> ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) )
44 24 25 43 syl2ani 
 |-  ( ( ( 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 ) ) -> ( ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) -> ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) )
45 44 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 ) ) ) /\ e e. ( EE ` N ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) ) -> ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) )
46 15 23 45 3jca 
 |-  ( ( ( ( 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 ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) ) -> ( ( e Btwn <. D , F >. /\ e Btwn <. D , F >. ) /\ ( <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. e , F >. ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) )
47 46 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 ) ) ) /\ e e. ( EE ` N ) ) -> ( ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) -> ( ( e Btwn <. D , F >. /\ e Btwn <. D , F >. ) /\ ( <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. e , F >. ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) ) )
48 brifs 
 |-  ( ( ( N e. NN /\ D e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ e e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( e e. ( EE ` N ) /\ F e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. <. D , e >. , <. F , e >. >. InnerFiveSeg <. <. D , e >. , <. F , E >. >. <-> ( ( e Btwn <. D , F >. /\ e Btwn <. D , F >. ) /\ ( <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. e , F >. ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) ) )
49 ifscgr 
 |-  ( ( ( N e. NN /\ D e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ e e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( e e. ( EE ` N ) /\ F e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. <. D , e >. , <. F , e >. >. InnerFiveSeg <. <. D , e >. , <. F , E >. >. -> <. e , e >. Cgr <. e , E >. ) )
50 48 49 sylbird 
 |-  ( ( ( N e. NN /\ D e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ e e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( e e. ( EE ` N ) /\ F e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( ( e Btwn <. D , F >. /\ e Btwn <. D , F >. ) /\ ( <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. e , F >. ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) -> <. e , e >. Cgr <. e , E >. ) )
51 16 17 20 18 20 17 20 18 33 50 syl333anc 
 |-  ( ( ( 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 ) ) -> ( ( ( e Btwn <. D , F >. /\ e Btwn <. D , F >. ) /\ ( <. D , F >. Cgr <. D , F >. /\ <. e , F >. Cgr <. e , F >. ) /\ ( <. D , e >. Cgr <. D , E >. /\ <. F , e >. Cgr <. F , E >. ) ) -> <. e , e >. Cgr <. e , E >. ) )
52 47 51 syld 
 |-  ( ( ( 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 ) ) -> ( ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) -> <. e , e >. Cgr <. e , E >. ) )
53 cgrid2 
 |-  ( ( N e. NN /\ ( e e. ( EE ` N ) /\ e e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. e , e >. Cgr <. e , E >. -> e = E ) )
54 16 20 20 33 53 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 e. ( EE ` N ) ) -> ( <. e , e >. Cgr <. e , E >. -> e = E ) )
55 52 54 syld 
 |-  ( ( ( 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 ) ) -> ( ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) -> e = E ) )
56 55 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 ) ) ) /\ e e. ( EE ` N ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) ) -> e = E )
57 56 14 eqbrtrrd 
 |-  ( ( ( ( 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 ) ) /\ ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) /\ ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) ) ) -> E Btwn <. D , F >. )
58 57 expr 
 |-  ( ( ( ( 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 ) ) /\ ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) ) -> ( ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) -> E Btwn <. D , F >. ) )
59 58 an32s 
 |-  ( ( ( ( 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 e. ( EE ` N ) ) -> ( ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) -> E Btwn <. D , F >. ) )
60 59 rexlimdva 
 |-  ( ( ( 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. e e. ( EE ` N ) ( e Btwn <. D , F >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. e , F >. >. ) -> E Btwn <. D , F >. ) )
61 13 60 mpd 
 |-  ( ( ( 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 >. )
62 61 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 ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. D , <. E , F >. >. ) -> E Btwn <. D , F >. ) )