MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfcgra2 Structured version   Visualization version   Unicode version

Theorem dfcgra2 24920
Description: This is the full statement of definition 11.2 of [Schwabhauser] p. 95. This proof serves to confirm that the definition we have chosen, df-cgra 24899 is indeed equivalent with the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.)
Hypotheses
Ref Expression
dfcgra2.p  |-  P  =  ( Base `  G
)
dfcgra2.i  |-  I  =  (Itv `  G )
dfcgra2.m  |-  .-  =  ( dist `  G )
dfcgra2.g  |-  ( ph  ->  G  e. TarskiG )
dfcgra2.a  |-  ( ph  ->  A  e.  P )
dfcgra2.b  |-  ( ph  ->  B  e.  P )
dfcgra2.c  |-  ( ph  ->  C  e.  P )
dfcgra2.d  |-  ( ph  ->  D  e.  P )
dfcgra2.e  |-  ( ph  ->  E  e.  P )
dfcgra2.f  |-  ( ph  ->  F  e.  P )
Assertion
Ref Expression
dfcgra2  |-  ( ph  ->  ( <" A B C "> (cgrA `  G ) <" D E F ">  <->  ( ( A  =/=  B  /\  C  =/=  B )  /\  ( D  =/=  E  /\  F  =/=  E )  /\  E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) ) ) )
Distinct variable groups:    .- , a, c, d, f    A, a, c, d, f    B, a, c, d, f    C, a, c, d, f    D, a, c, d, f    E, a, c, d, f    F, a, c, d, f    G, a, c, d, f    I,
a, c, d, f    P, a, c, d, f    ph, a, c, d, f

Proof of Theorem dfcgra2
Dummy variables  t  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfcgra2.p . . . . 5  |-  P  =  ( Base `  G
)
2 dfcgra2.i . . . . 5  |-  I  =  (Itv `  G )
3 eqid 2462 . . . . 5  |-  (hlG `  G )  =  (hlG
`  G )
4 dfcgra2.g . . . . . 6  |-  ( ph  ->  G  e. TarskiG )
54adantr 471 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  G  e. TarskiG )
6 dfcgra2.a . . . . . 6  |-  ( ph  ->  A  e.  P )
76adantr 471 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  A  e.  P )
8 dfcgra2.b . . . . . 6  |-  ( ph  ->  B  e.  P )
98adantr 471 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  B  e.  P )
10 dfcgra2.c . . . . . 6  |-  ( ph  ->  C  e.  P )
1110adantr 471 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  C  e.  P )
12 dfcgra2.d . . . . . 6  |-  ( ph  ->  D  e.  P )
1312adantr 471 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  D  e.  P )
14 dfcgra2.e . . . . . 6  |-  ( ph  ->  E  e.  P )
1514adantr 471 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  E  e.  P )
16 dfcgra2.f . . . . . 6  |-  ( ph  ->  F  e.  P )
1716adantr 471 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  F  e.  P )
18 simpr 467 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  <" A B C "> (cgrA `  G ) <" D E F "> )
191, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane1 24903 . . . 4  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  A  =/=  B )
201, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane2 24904 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  B  =/=  C )
2120necomd 2691 . . . 4  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  C  =/=  B )
2219, 21jca 539 . . 3  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  ( A  =/=  B  /\  C  =/=  B
) )
231, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane3 24905 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  E  =/=  D )
2423necomd 2691 . . . 4  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  D  =/=  E )
251, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane4 24906 . . . . 5  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  E  =/=  F )
2625necomd 2691 . . . 4  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  F  =/=  E )
2724, 26jca 539 . . 3  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  ( D  =/=  E  /\  F  =/=  E
) )
28 simprl 769 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  (
( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F
) ) ) )
29 simprr 771 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  (
( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C
) ) ) )
305ad5antr 745 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  G  e. TarskiG )
31 simp-5r 784 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  a  e.  P )
329ad5antr 745 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  B  e.  P )
33 simp-4r 782 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  c  e.  P )
34 simpllr 774 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  d  e.  P )
3515ad5antr 745 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  E  e.  P )
36 simplr 767 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  f  e.  P )
3717ad5antr 745 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  F  e.  P )
3813ad5antr 745 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  D  e.  P )
3911ad5antr 745 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  C  e.  P )
407ad5antr 745 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  A  e.  P )
4118ad5antr 745 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  <" A B C "> (cgrA `  G ) <" D E F "> )
421, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41cgracom 24913 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  <" D E F "> (cgrA `  G ) <" A B C "> )
4328simplld 766 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  A  e.  ( B I a ) )
44 dfcgra2.m . . . . . . . . . . . . . . . . . 18  |-  .-  =  ( dist `  G )
4519ad5antr 745 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  A  =/=  B )
461, 44, 2, 30, 32, 40, 31, 43, 45tgbtwnne 24583 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  B  =/=  a )
471, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45btwnhl1 24706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  A
( (hlG `  G
) `  B )
a )
481, 2, 3, 40, 31, 32, 30, 47hlcomd 24698 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  a
( (hlG `  G
) `  B ) A )
491, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48cgrahl1 24907 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  <" D E F "> (cgrA `  G ) <" a B C "> )
5028simprld 770 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  C  e.  ( B I c ) )
5121ad5antr 745 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  C  =/=  B )
521, 44, 2, 30, 32, 39, 33, 50, 51tgbtwnne 24583 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  B  =/=  c )
531, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51btwnhl1 24706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  C
( (hlG `  G
) `  B )
c )
541, 2, 3, 39, 33, 32, 30, 53hlcomd 24698 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  c
( (hlG `  G
) `  B ) C )
551, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54cgrahl2 24908 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  <" D E F "> (cgrA `  G ) <" a B c "> )
561, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55cgracom 24913 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  <" a B c "> (cgrA `  G ) <" D E F "> )
5729simplld 766 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  D  e.  ( E I d ) )
5824ad5antr 745 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  D  =/=  E )
591, 44, 2, 30, 35, 38, 34, 57, 58tgbtwnne 24583 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  E  =/=  d )
601, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58btwnhl1 24706 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  D
( (hlG `  G
) `  E )
d )
611, 2, 3, 38, 34, 35, 30, 60hlcomd 24698 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  d
( (hlG `  G
) `  E ) D )
621, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61cgrahl1 24907 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  <" a B c "> (cgrA `  G ) <" d E F "> )
6329simprld 770 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  F  e.  ( E I f ) )
6426ad5antr 745 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  F  =/=  E )
651, 44, 2, 30, 35, 37, 36, 63, 64tgbtwnne 24583 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  E  =/=  f )
661, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64btwnhl1 24706 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  F
( (hlG `  G
) `  E )
f )
671, 2, 3, 37, 36, 35, 30, 66hlcomd 24698 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  f
( (hlG `  G
) `  E ) F )
681, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67cgrahl2 24908 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  <" a B c "> (cgrA `  G ) <" d E f "> )
691, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68cgrane1 24903 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  a  =/=  B )
701, 2, 3, 31, 40, 32, 30, 69hlid 24703 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  a
( (hlG `  G
) `  B )
a )
711, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68cgrane2 24904 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  B  =/=  c )
7271necomd 2691 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  c  =/=  B )
731, 2, 3, 33, 40, 32, 30, 72hlid 24703 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  c
( (hlG `  G
) `  B )
c )
741, 44, 2, 30, 32, 40, 31, 43tgbtwncom 24581 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  A  e.  ( a I B ) )
7528simplrd 768 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( A  .-  a )  =  ( E  .-  D
) )
761, 44, 2, 30, 40, 31, 35, 38, 75tgcgrcoml 24572 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  (
a  .-  A )  =  ( E  .-  D ) )
7729simplrd 768 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( D  .-  d )  =  ( B  .-  A
) )
7877eqcomd 2468 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( B  .-  A )  =  ( D  .-  d
) )
791, 44, 2, 30, 32, 40, 38, 34, 78tgcgrcoml 24572 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( A  .-  B )  =  ( D  .-  d
) )
801, 44, 2, 30, 31, 40, 32, 35, 38, 34, 74, 57, 76, 79tgcgrextend 24578 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  (
a  .-  B )  =  ( E  .-  d ) )
811, 44, 2, 30, 31, 32, 35, 34, 80tgcgrcoml 24572 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( B  .-  a )  =  ( E  .-  d
) )
821, 44, 2, 30, 32, 39, 33, 50tgbtwncom 24581 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  C  e.  ( c I B ) )
8328simprrd 772 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( C  .-  c )  =  ( E  .-  F
) )
841, 44, 2, 30, 39, 33, 35, 37, 83tgcgrcoml 24572 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  (
c  .-  C )  =  ( E  .-  F ) )
8529simprrd 772 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( F  .-  f )  =  ( B  .-  C
) )
8685eqcomd 2468 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( B  .-  C )  =  ( F  .-  f
) )
871, 44, 2, 30, 32, 39, 37, 36, 86tgcgrcoml 24572 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( C  .-  B )  =  ( F  .-  f
) )
881, 44, 2, 30, 33, 39, 32, 35, 37, 36, 82, 63, 84, 87tgcgrextend 24578 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  (
c  .-  B )  =  ( E  .-  f ) )
891, 44, 2, 30, 33, 32, 35, 36, 88tgcgrcoml 24572 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  ( B  .-  c )  =  ( E  .-  f
) )
901, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 73, 81, 89cgracgr 24909 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  (
a  .-  c )  =  ( d  .-  f ) )
9128, 29, 903jca 1194 . . . . . . . 8  |-  ( ( ( ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P )  /\  c  e.  P
)  /\  d  e.  P )  /\  f  e.  P )  /\  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) )
9291ex 440 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P
)  /\  c  e.  P )  /\  d  e.  P )  /\  f  e.  P )  ->  (
( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )  ->  ( (
( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F
) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) ) )
9392reximdva 2874 . . . . . 6  |-  ( ( ( ( ( ph  /\ 
<" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P
)  /\  c  e.  P )  /\  d  e.  P )  ->  ( E. f  e.  P  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )  ->  E. f  e.  P  ( (
( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F
) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) ) )
9493reximdva 2874 . . . . 5  |-  ( ( ( ( ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P
)  /\  c  e.  P )  ->  ( E. d  e.  P  E. f  e.  P  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )  ->  E. d  e.  P  E. f  e.  P  ( (
( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F
) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) ) )
9594imp 435 . . . 4  |-  ( ( ( ( ( ph  /\ 
<" A B C "> (cgrA `  G ) <" D E F "> )  /\  a  e.  P
)  /\  c  e.  P )  /\  E. d  e.  P  E. f  e.  P  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )  ->  E. d  e.  P  E. f  e.  P  ( (
( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F
) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) )
961, 44, 2, 4, 8, 6, 14, 12axtgsegcon 24561 . . . . . . . 8  |-  ( ph  ->  E. a  e.  P  ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) ) )
971, 44, 2, 4, 8, 10, 14, 16axtgsegcon 24561 . . . . . . . 8  |-  ( ph  ->  E. c  e.  P  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )
98 reeanv 2970 . . . . . . . 8  |-  ( E. a  e.  P  E. c  e.  P  (
( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F
) ) )  <->  ( E. a  e.  P  ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  E. c  e.  P  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) ) )
9996, 97, 98sylanbrc 675 . . . . . . 7  |-  ( ph  ->  E. a  e.  P  E. c  e.  P  ( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) ) )
1001, 44, 2, 4, 14, 12, 8, 6axtgsegcon 24561 . . . . . . . 8  |-  ( ph  ->  E. d  e.  P  ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) ) )
1011, 44, 2, 4, 14, 16, 8, 10axtgsegcon 24561 . . . . . . . 8  |-  ( ph  ->  E. f  e.  P  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )
102 reeanv 2970 . . . . . . . 8  |-  ( E. d  e.  P  E. f  e.  P  (
( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C
) ) )  <->  ( E. d  e.  P  ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) )  /\  E. f  e.  P  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )
103100, 101, 102sylanbrc 675 . . . . . . 7  |-  ( ph  ->  E. d  e.  P  E. f  e.  P  ( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )
10499, 103jca 539 . . . . . 6  |-  ( ph  ->  ( E. a  e.  P  E. c  e.  P  ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  E. d  e.  P  E. f  e.  P  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )
105 r19.41vv 2956 . . . . . . . . 9  |-  ( E. d  e.  P  E. f  e.  P  (
( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) ) )  <->  ( E. d  e.  P  E. f  e.  P  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  (
( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F
) ) ) ) )
106 ancom 456 . . . . . . . . . 10  |-  ( ( ( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) ) )  <->  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  (
( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C
) ) ) ) )
1071062rexbii 2902 . . . . . . . . 9  |-  ( E. d  e.  P  E. f  e.  P  (
( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) ) )  <->  E. d  e.  P  E. f  e.  P  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )
108 ancom 456 . . . . . . . . 9  |-  ( ( E. d  e.  P  E. f  e.  P  ( ( D  e.  ( E I d )  /\  ( D 
.-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) ) )  <->  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  E. d  e.  P  E. f  e.  P  (
( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C
) ) ) ) )
109105, 107, 1083bitr3i 283 . . . . . . . 8  |-  ( E. d  e.  P  E. f  e.  P  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )  <->  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  E. d  e.  P  E. f  e.  P  (
( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C
) ) ) ) )
1101092rexbii 2902 . . . . . . 7  |-  ( E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )  <->  E. a  e.  P  E. c  e.  P  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  E. d  e.  P  E. f  e.  P  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )
111 r19.41vv 2956 . . . . . . 7  |-  ( E. a  e.  P  E. c  e.  P  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  E. d  e.  P  E. f  e.  P  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )  <->  ( E. a  e.  P  E. c  e.  P  ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  E. d  e.  P  E. f  e.  P  (
( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A ) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C
) ) ) ) )
112110, 111bitr2i 258 . . . . . 6  |-  ( ( E. a  e.  P  E. c  e.  P  ( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  E. d  e.  P  E. f  e.  P  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) )  <->  E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )
113104, 112sylib 201 . . . . 5  |-  ( ph  ->  E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )
114113adantr 471 . . . 4  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) ) ) )
11595, 114reximddv2 2876 . . 3  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  ( ( ( A  e.  ( B I a )  /\  ( A  .-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) )
11622, 27, 1153jca 1194 . 2  |-  ( (
ph  /\  <" A B C "> (cgrA `  G ) <" D E F "> )  ->  ( ( A  =/= 
B  /\  C  =/=  B )  /\  ( D  =/=  E  /\  F  =/=  E )  /\  E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) ) )
117 df-3an 993 . . 3  |-  ( ( ( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E )  /\  E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) )  <->  ( (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) )  /\  E. a  e.  P  E. c  e.  P  E. d  e.  P  E. f  e.  P  (
( ( A  e.  ( B I a )  /\  ( A 
.-  a )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I c )  /\  ( C  .-  c )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I d )  /\  ( D  .-  d )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I f )  /\  ( F  .-  f )  =  ( B  .-  C ) ) )  /\  ( a  .-  c )  =  ( d  .-  f ) ) ) )
1184ad6antr 747 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  G  e. TarskiG )
11912ad6antr 747 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  D  e.  P )
12014ad6antr 747 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  E  e.  P )
12116ad6antr 747 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  F  e.  P )
1226ad6antr 747 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  A  e.  P )
1238ad6antr 747 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  B  e.  P )
12410ad6antr 747 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  C  e.  P )
125 simp-4r 782 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  y  e.  P )
126 simp-5r 784 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  x  e.  P )
127 simpllr 774 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  z  e.  P )
128 simplr 767 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  t  e.  P )
129 eqid 2462 . . . . . . . . . . . . . 14  |-  (cgrG `  G )  =  (cgrG `  G )
130 simpr1 1020 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  (
( A  e.  ( B I x )  /\  ( A  .-  x )  =  ( E  .-  D ) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F
) ) ) )
131130simplld 766 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B  .-  C ) ) )  /\  ( x  .-  y )  =  ( z  .-  t ) ) )  ->  A  e.  ( B I x ) )
132 simpr2 1021 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  (
( A  =/=  B  /\  C  =/=  B
)  /\  ( D  =/=  E  /\  F  =/= 
E ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  z  e.  P )  /\  t  e.  P )  /\  (
( ( A  e.  ( B I x )  /\  ( A 
.-  x )  =  ( E  .-  D
) )  /\  ( C  e.  ( B I y )  /\  ( C  .-  y )  =  ( E  .-  F ) ) )  /\  ( ( D  e.  ( E I z )  /\  ( D  .-  z )  =  ( B  .-  A
) )  /\  ( F  e.  ( E I t )  /\  ( F  .-  t )  =  ( B