Metamath Proof Explorer

Theorem seglecgr12im

Description: Substitution law for segment comparison under congruence. Theorem 5.6 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion seglecgr12im 
|- ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. /\ <. A , B >. Seg<_ <. C , D >. ) -> <. E , F >. Seg<_ <. G , H >. ) )

Proof

Step Hyp Ref Expression
1 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> y Btwn <. C , D >. )
2 simprlr 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> <. C , D >. Cgr <. G , H >. )
3 simpl11 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> N e. NN )
4 simpl21 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> C e. ( EE ` N ) )
5 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> y e. ( EE ` N ) )
6 simpl22 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> D e. ( EE ` N ) )
7 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> G e. ( EE ` N ) )
8 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> H e. ( EE ` N ) )
9 cgrxfr 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( y Btwn <. C , D >. /\ <. C , D >. Cgr <. G , H >. ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. ) ) )
10 3 4 5 6 7 8 9 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> ( ( y Btwn <. C , D >. /\ <. C , D >. Cgr <. G , H >. ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. ) ) )
11 10 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> ( ( y Btwn <. C , D >. /\ <. C , D >. Cgr <. G , H >. ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. ) ) )
12 1 2 11 mp2and 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. ) )
13 anass 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ z e. ( EE ` N ) ) <-> ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) )
14 simpl11 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> N e. NN )
15 simpl21 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
16 simprl 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> y e. ( EE ` N ) )
17 simpl22 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
18 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
19 simprr 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> z e. ( EE ` N ) )
20 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> H e. ( EE ` N ) )
21 brcgr3 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ z e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. <-> ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) )
22 14 15 16 17 18 19 20 21 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> ( <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. <-> ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) )
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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> ( <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. <-> ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) )
24 df-3an 
 |-  ( ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) <-> ( ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) /\ ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) )
25 simpl23 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
26 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
27 simpl12 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
28 simpl13 
 |-  ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
29 simpr1l 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) ) -> <. A , B >. Cgr <. E , F >. )
30 simpr2r 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) ) -> <. A , B >. Cgr <. C , y >. )
31 14 27 28 25 26 15 16 29 30 cgrtr4and 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) ) -> <. E , F >. Cgr <. C , y >. )
32 simpr31 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) ) -> <. C , y >. Cgr <. G , z >. )
33 14 25 26 15 16 18 19 31 32 cgrtrand 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) ) -> <. E , F >. Cgr <. G , z >. )
34 24 33 sylan2br 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) /\ ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) ) ) -> <. E , F >. Cgr <. G , z >. )
35 34 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> ( ( <. C , y >. Cgr <. G , z >. /\ <. C , D >. Cgr <. G , H >. /\ <. y , D >. Cgr <. z , H >. ) -> <. E , F >. Cgr <. G , z >. ) )
36 23 35 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> ( <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. -> <. E , F >. Cgr <. G , z >. ) )
37 36 anim2d 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> ( ( z Btwn <. G , H >. /\ <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. ) -> ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
38 13 37 sylanb 
 |-  ( ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ z e. ( EE ` N ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> ( ( z Btwn <. G , H >. /\ <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. ) -> ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
39 38 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) /\ z e. ( EE ` N ) ) -> ( ( z Btwn <. G , H >. /\ <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. ) -> ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
40 39 reximdva 
 |-  ( ( ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> ( E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. C , <. y , D >. >. Cgr3 <. G , <. z , H >. >. ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
41 12 40 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) )
42 41 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
43 42 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ y e. ( EE ` N ) ) -> ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
44 43 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) -> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
45 simp11 
 |-  ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> N e. NN )
46 simp12 
 |-  ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
47 simp13 
 |-  ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
48 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
49 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
50 brsegle 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
51 45 46 47 48 49 50 syl122anc 
 |-  ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
52 51 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
53 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
54 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
55 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
56 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> H e. ( EE ` N ) )
57 brsegle 
 |-  ( ( N e. NN /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. E , F >. Seg<_ <. G , H >. <-> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
58 45 53 54 55 56 57 syl122anc 
 |-  ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. E , F >. Seg<_ <. G , H >. <-> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
59 58 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( <. E , F >. Seg<_ <. G , H >. <-> E. z e. ( EE ` N ) ( z Btwn <. G , H >. /\ <. E , F >. Cgr <. G , z >. ) ) )
60 44 52 59 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( <. A , B >. Seg<_ <. C , D >. -> <. E , F >. Seg<_ <. G , H >. ) )
61 60 exp32 
 |-  ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. E , F >. -> ( <. C , D >. Cgr <. G , H >. -> ( <. A , B >. Seg<_ <. C , D >. -> <. E , F >. Seg<_ <. G , H >. ) ) ) )
62 61 3impd 
 |-  ( ( ( 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 ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. G , H >. /\ <. A , B >. Seg<_ <. C , D >. ) -> <. E , F >. Seg<_ <. G , H >. ) )