Metamath Proof Explorer

Theorem dfcgra2

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 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses 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 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfcgra2.p 
 |-  P = ( Base ` G )
2 dfcgra2.i 
 |-  I = ( Itv ` G )
3 dfcgra2.m 
 |-  .- = ( dist ` G )
4 dfcgra2.g 
 |-  ( ph -> G e. TarskiG )
5 dfcgra2.a 
 |-  ( ph -> A e. P )
6 dfcgra2.b 
 |-  ( ph -> B e. P )
7 dfcgra2.c 
 |-  ( ph -> C e. P )
8 dfcgra2.d 
 |-  ( ph -> D e. P )
9 dfcgra2.e 
 |-  ( ph -> E e. P )
10 dfcgra2.f 
 |-  ( ph -> F e. P )
11 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
12 4 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> G e. TarskiG )
13 5 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> A e. P )
14 6 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> B e. P )
15 7 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> C e. P )
16 8 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> D e. P )
17 9 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> E e. P )
18 10 adantr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> F e. P )
19 simpr 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
20 1 2 11 12 13 14 15 16 17 18 19 cgrane1 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> A =/= B )
21 1 2 11 12 13 14 15 16 17 18 19 cgrane2 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> B =/= C )
22 21 necomd 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> C =/= B )
23 20 22 jca 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> ( A =/= B /\ C =/= B ) )
24 1 2 11 12 13 14 15 16 17 18 19 cgrane3 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> E =/= D )
25 24 necomd 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> D =/= E )
26 1 2 11 12 13 14 15 16 17 18 19 cgrane4 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> E =/= F )
27 26 necomd 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> F =/= E )
28 25 27 jca 
 |-  ( ( ph /\ <" A B C "> ( cgrA ` G ) <" D E F "> ) -> ( D =/= E /\ F =/= E ) )
29 simprl 
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
30 simprr 
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
31 4 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
32 simp-5r 
 |-  ( ( ( ( ( ( ( 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 )
33 6 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
34 simp-4r 
 |-  ( ( ( ( ( ( ( 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 )
35 simpllr 
 |-  ( ( ( ( ( ( ( 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 )
36 9 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
37 simplr 
 |-  ( ( ( ( ( ( ( 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 )
38 10 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
39 8 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
40 7 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
41 5 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
42 simp-6r 
 |-  ( ( ( ( ( ( ( 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 "> )
43 1 2 31 11 41 33 40 39 36 38 42 cgracom 
 |-  ( ( ( ( ( ( ( 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 "> )
44 29 simplld 
 |-  ( ( ( ( ( ( ( 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 ) )
45 20 ad5antr 
 |-  ( ( ( ( ( ( ( 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 )
46 1 3 2 31 33 41 32 44 45 tgbtwnne 
 |-  ( ( ( ( ( ( ( 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 )
47 1 2 11 33 32 41 31 41 44 46 45 btwnhl1 
 |-  ( ( ( ( ( ( ( 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 )
48 1 2 11 41 32 33 31 47 hlcomd 
 |-  ( ( ( ( ( ( ( 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 )
49 1 2 11 31 39 36 38 41 33 40 43 32 48 cgrahl1 
 |-  ( ( ( ( ( ( ( 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 "> )
50 29 simprld 
 |-  ( ( ( ( ( ( ( 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 ) )
51 22 ad5antr 
 |-  ( ( ( ( ( ( ( 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 )
52 1 3 2 31 33 40 34 50 51 tgbtwnne 
 |-  ( ( ( ( ( ( ( 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 )
53 1 2 11 33 34 40 31 41 50 52 51 btwnhl1 
 |-  ( ( ( ( ( ( ( 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 )
54 1 2 11 40 34 33 31 53 hlcomd 
 |-  ( ( ( ( ( ( ( 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 )
55 1 2 11 31 39 36 38 32 33 40 49 34 54 cgrahl2 
 |-  ( ( ( ( ( ( ( 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 "> )
56 1 2 31 11 39 36 38 32 33 34 55 cgracom 
 |-  ( ( ( ( ( ( ( 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 "> )
57 30 simplld 
 |-  ( ( ( ( ( ( ( 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 ) )
58 25 ad5antr 
 |-  ( ( ( ( ( ( ( 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 )
59 1 3 2 31 36 39 35 57 58 tgbtwnne 
 |-  ( ( ( ( ( ( ( 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 )
60 1 2 11 36 35 39 31 41 57 59 58 btwnhl1 
 |-  ( ( ( ( ( ( ( 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 )
61 1 2 11 39 35 36 31 60 hlcomd 
 |-  ( ( ( ( ( ( ( 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 )
62 1 2 11 31 32 33 34 39 36 38 56 35 61 cgrahl1 
 |-  ( ( ( ( ( ( ( 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 "> )
63 30 simprld 
 |-  ( ( ( ( ( ( ( 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 ) )
64 27 ad5antr 
 |-  ( ( ( ( ( ( ( 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 )
65 1 3 2 31 36 38 37 63 64 tgbtwnne 
 |-  ( ( ( ( ( ( ( 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 )
66 1 2 11 36 37 38 31 41 63 65 64 btwnhl1 
 |-  ( ( ( ( ( ( ( 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 )
67 1 2 11 38 37 36 31 66 hlcomd 
 |-  ( ( ( ( ( ( ( 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 )
68 1 2 11 31 32 33 34 35 36 38 62 37 67 cgrahl2 
 |-  ( ( ( ( ( ( ( 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 "> )
69 46 necomd 
 |-  ( ( ( ( ( ( ( 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 )
70 1 2 11 32 41 33 31 69 hlid 
 |-  ( ( ( ( ( ( ( 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 )
71 52 necomd 
 |-  ( ( ( ( ( ( ( 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 )
72 1 2 11 34 41 33 31 71 hlid 
 |-  ( ( ( ( ( ( ( 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 )
73 1 3 2 31 33 41 32 44 tgbtwncom 
 |-  ( ( ( ( ( ( ( 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 ) )
74 29 simplrd 
 |-  ( ( ( ( ( ( ( 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 ) )
75 1 3 2 31 41 32 36 39 74 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 ) )
76 30 simplrd 
 |-  ( ( ( ( ( ( ( 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 ) )
77 76 eqcomd 
 |-  ( ( ( ( ( ( ( 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 ) )
78 1 3 2 31 33 41 39 35 77 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 ) )
79 1 3 2 31 32 41 33 36 39 35 73 57 75 78 tgcgrextend 
 |-  ( ( ( ( ( ( ( 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 ) )
80 1 3 2 31 32 33 36 35 79 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 ) )
81 1 3 2 31 33 40 34 50 tgbtwncom 
 |-  ( ( ( ( ( ( ( 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 ) )
82 29 simprrd 
 |-  ( ( ( ( ( ( ( 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 ) )
83 1 3 2 31 40 34 36 38 82 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 ) )
84 30 simprrd 
 |-  ( ( ( ( ( ( ( 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 ) )
85 84 eqcomd 
 |-  ( ( ( ( ( ( ( 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 ) )
86 1 3 2 31 33 40 38 37 85 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 ) )
87 1 3 2 31 34 40 33 36 38 37 81 63 83 86 tgcgrextend 
 |-  ( ( ( ( ( ( ( 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 ) )
88 1 3 2 31 34 33 36 37 87 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 ) )
89 1 2 11 31 32 33 34 35 36 37 68 32 3 34 70 72 80 88 cgracgr 
 |-  ( ( ( ( ( ( ( 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 ) )
90 29 30 89 3jca 
 |-  ( ( ( ( ( ( ( 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 ) ) )
91 90 ex 
 |-  ( ( ( ( ( ( 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 ) ) ) )
92 91 reximdva 
 |-  ( ( ( ( ( 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 ) ) ) )
93 92 reximdva 
 |-  ( ( ( ( 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 ) ) ) )
94 93 imp 
 |-  ( ( ( ( ( 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 ) ) )
95 1 3 2 4 6 5 9 8 axtgsegcon 
 |-  ( ph -> E. a e. P ( A e. ( B I a ) /\ ( A .- a ) = ( E .- D ) ) )
96 1 3 2 4 6 7 9 10 axtgsegcon 
 |-  ( ph -> E. c e. P ( C e. ( B I c ) /\ ( C .- c ) = ( E .- F ) ) )
97 reeanv 
 |-  ( 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 ) ) ) )
98 95 96 97 sylanbrc 
 |-  ( 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 ) ) ) )
99 1 3 2 4 9 8 6 5 axtgsegcon 
 |-  ( ph -> E. d e. P ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) )
100 1 3 2 4 9 10 6 7 axtgsegcon 
 |-  ( ph -> E. f e. P ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) )
101 reeanv 
 |-  ( 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 ) ) ) )
102 99 100 101 sylanbrc 
 |-  ( 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 ) ) ) )
103 98 102 jca 
 |-  ( 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 ) ) ) ) )
104 r19.41vv 
 |-  ( 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 ) ) ) ) )
105 ancom 
 |-  ( ( ( ( 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 ) ) ) ) )
106 105 2rexbii 
 |-  ( 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 ) ) ) ) )
107 ancom 
 |-  ( ( 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 ) ) ) ) )
108 104 106 107 3bitr3i 
 |-  ( 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 ) ) ) ) )
109 108 2rexbii 
 |-  ( 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 ) ) ) ) )
110 r19.41vv 
 |-  ( 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 ) ) ) ) )
111 109 110 bitr2i 
 |-  ( ( 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 ) ) ) ) )
112 103 111 sylib 
 |-  ( 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 ) ) ) ) )
113 112 adantr 
 |-  ( ( 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 ) ) ) ) )
114 94 113 reximddv2 
 |-  ( ( 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 ) ) )
115 23 28 114 3jca 
 |-  ( ( 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 ) ) ) )
116 df-3an 
 |-  ( ( ( 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 ) ) ) )
117 4 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
118 8 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
119 9 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
120 10 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
121 5 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
122 6 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
123 7 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
124 simp-4r 
 |-  ( ( ( ( ( ( ( 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 )
125 simp-5r 
 |-  ( ( ( ( ( ( ( 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 )
126 simpllr 
 |-  ( ( ( ( ( ( ( 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 )
127 simplr 
 |-  ( ( ( ( ( ( ( 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 )
128 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
129 simpr1 
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
130 129 simplld 
 |-  ( ( ( ( ( ( ( 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 ) )
131 simpr2 
 |-  ( ( ( ( ( ( ( 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. ( E I z ) /\ ( D .- z ) = ( B .- A ) ) /\ ( F e. ( E I t ) /\ ( F .- t ) = ( B .- C ) ) ) )
132 131 simplld 
 |-  ( ( ( ( ( ( ( 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. ( E I z ) )
133 1 3 2 117 119 118 126 132 tgbtwncom 
 |-  ( ( ( ( ( ( ( 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. ( z I E ) )
134 131 simplrd 
 |-  ( ( ( ( ( ( ( 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 .- z ) = ( B .- A ) )
135 134 eqcomd 
 |-  ( ( ( ( ( ( ( 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 .- A ) = ( D .- z ) )
136 1 3 2 117 122 121 118 126 135 tgcgrcomr 
 |-  ( ( ( ( ( ( ( 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 .- A ) = ( z .- D ) )
137 129 simplrd 
 |-  ( ( ( ( ( ( ( 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 .- x ) = ( E .- D ) )
138 1 3 2 117 121 125 119 118 137 tgcgrcomr 
 |-  ( ( ( ( ( ( ( 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 .- x ) = ( D .- E ) )
139 1 3 2 117 122 121 125 126 118 119 130 133 136 138 tgcgrextend 
 |-  ( ( ( ( ( ( ( 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 .- x ) = ( z .- E ) )
140 1 3 2 117 122 125 126 119 139 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 .- B ) = ( z .- E ) )
141 129 simprld 
 |-  ( ( ( ( ( ( ( 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. ( B I y ) )
142 1 3 2 117 122 123 124 141 tgbtwncom 
 |-  ( ( ( ( ( ( ( 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. ( y I B ) )
143 131 simprld 
 |-  ( ( ( ( ( ( ( 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. ( E I t ) )
144 129 simprrd 
 |-  ( ( ( ( ( ( ( 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 .- y ) = ( E .- F ) )
145 1 3 2 117 123 124 119 120 144 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 .- C ) = ( E .- F ) )
146 131 simprrd 
 |-  ( ( ( ( ( ( ( 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 .- t ) = ( B .- C ) )
147 146 eqcomd 
 |-  ( ( ( ( ( ( ( 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 .- C ) = ( F .- t ) )
148 1 3 2 117 122 123 120 127 147 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 .- B ) = ( F .- t ) )
149 1 3 2 117 124 123 122 119 120 127 142 143 145 148 tgcgrextend 
 |-  ( ( ( ( ( ( ( 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 .- B ) = ( E .- t ) )
150 1 3 2 117 124 122 119 127 149 tgcgrcoml 
 |-  ( ( ( ( ( ( ( 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 .- y ) = ( E .- t ) )
151 simpr3 
 |-  ( ( ( ( ( ( ( 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 .- y ) = ( z .- t ) )
152 1 3 2 117 125 124 126 127 151 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( 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 .- x ) = ( t .- z ) )
153 1 3 128 117 125 122 124 126 119 127 140 150 152 trgcgr 
 |-  ( ( ( ( ( ( ( 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 B y "> ( cgrG ` G ) <" z E t "> )
154 simp-6r 
 |-  ( ( ( ( ( ( ( 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 =/= B /\ C =/= B ) /\ ( D =/= E /\ F =/= E ) ) )
155 154 simprld 
 |-  ( ( ( ( ( ( ( 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 )
156 1 3 2 117 119 118 126 132 155 tgbtwnne 
 |-  ( ( ( ( ( ( ( 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 =/= z )
157 1 2 11 119 126 118 117 122 132 156 155 btwnhl1 
 |-  ( ( ( ( ( ( ( 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 ( ( hlG ` G ) ` E ) z )
158 1 2 11 118 126 119 117 157 hlcomd 
 |-  ( ( ( ( ( ( ( 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 ( ( hlG ` G ) ` E ) D )
159 154 simprrd 
 |-  ( ( ( ( ( ( ( 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 )
160 1 3 2 117 119 120 127 143 159 tgbtwnne 
 |-  ( ( ( ( ( ( ( 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 =/= t )
161 1 2 11 119 127 120 117 122 143 160 159 btwnhl1 
 |-  ( ( ( ( ( ( ( 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 ( ( hlG ` G ) ` E ) t )
162 1 2 11 120 127 119 117 161 hlcomd 
 |-  ( ( ( ( ( ( ( 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 ( ( hlG ` G ) ` E ) F )
163 1 2 11 117 125 122 124 118 119 120 126 127 153 158 162 iscgrad 
 |-  ( ( ( ( ( ( ( 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 B y "> ( cgrA ` G ) <" D E F "> )
164 1 2 117 11 125 122 124 118 119 120 163 cgracom 
 |-  ( ( ( ( ( ( ( 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 F "> ( cgrA ` G ) <" x B y "> )
165 154 simplld 
 |-  ( ( ( ( ( ( ( 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 =/= B )
166 1 3 2 117 122 121 125 130 165 tgbtwnne 
 |-  ( ( ( ( ( ( ( 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 =/= x )
167 1 2 11 122 125 121 117 121 130 166 165 btwnhl1 
 |-  ( ( ( ( ( ( ( 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 ( ( hlG ` G ) ` B ) x )
168 1 2 11 117 118 119 120 125 122 124 164 121 167 cgrahl1 
 |-  ( ( ( ( ( ( ( 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 F "> ( cgrA ` G ) <" A B y "> )
169 154 simplrd 
 |-  ( ( ( ( ( ( ( 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 =/= B )
170 1 3 2 117 122 123 124 141 169 tgbtwnne 
 |-  ( ( ( ( ( ( ( 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 =/= y )
171 1 2 11 122 124 123 117 121 141 170 169 btwnhl1 
 |-  ( ( ( ( ( ( ( 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 ( ( hlG ` G ) ` B ) y )
172 1 2 11 117 118 119 120 121 122 124 168 123 171 cgrahl2 
 |-  ( ( ( ( ( ( ( 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 F "> ( cgrA ` G ) <" A B C "> )
173 1 2 117 11 118 119 120 121 122 123 172 cgracom 
 |-  ( ( ( ( ( ( ( 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 B C "> ( cgrA ` G ) <" D E F "> )
174 173 adantl3r 
 |-  ( ( ( ( ( ( ( ( ph /\ ( ( A =/= B /\ C =/= B ) /\ ( D =/= E /\ F =/= E ) ) ) /\ x e. P ) /\ y e. P ) /\ E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) ) /\ 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 B C "> ( cgrA ` G ) <" D E F "> )
175 simpr 
 |-  ( ( ( ( ( ph /\ ( ( A =/= B /\ C =/= B ) /\ ( D =/= E /\ F =/= E ) ) ) /\ x e. P ) /\ y e. P ) /\ E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) ) -> E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) )
176 oveq2 
 |-  ( d = z -> ( E I d ) = ( E I z ) )
177 176 eleq2d 
 |-  ( d = z -> ( D e. ( E I d ) <-> D e. ( E I z ) ) )
178 oveq2 
 |-  ( d = z -> ( D .- d ) = ( D .- z ) )
179 178 eqeq1d 
 |-  ( d = z -> ( ( D .- d ) = ( B .- A ) <-> ( D .- z ) = ( B .- A ) ) )
180 177 179 anbi12d 
 |-  ( d = z -> ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) <-> ( D e. ( E I z ) /\ ( D .- z ) = ( B .- A ) ) ) )
181 180 anbi1d 
 |-  ( d = z -> ( ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) <-> ( ( D e. ( E I z ) /\ ( D .- z ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) ) )
182 oveq1 
 |-  ( d = z -> ( d .- f ) = ( z .- f ) )
183 182 eqeq2d 
 |-  ( d = z -> ( ( x .- y ) = ( d .- f ) <-> ( x .- y ) = ( z .- f ) ) )
184 181 183 3anbi23d 
 |-  ( d = z -> ( ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) <-> ( ( ( 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 f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( z .- f ) ) ) )
185 oveq2 
 |-  ( f = t -> ( E I f ) = ( E I t ) )
186 185 eleq2d 
 |-  ( f = t -> ( F e. ( E I f ) <-> F e. ( E I t ) ) )
187 oveq2 
 |-  ( f = t -> ( F .- f ) = ( F .- t ) )
188 187 eqeq1d 
 |-  ( f = t -> ( ( F .- f ) = ( B .- C ) <-> ( F .- t ) = ( B .- C ) ) )
189 186 188 anbi12d 
 |-  ( f = t -> ( ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) <-> ( F e. ( E I t ) /\ ( F .- t ) = ( B .- C ) ) ) )
190 189 anbi2d 
 |-  ( f = t -> ( ( ( D e. ( E I z ) /\ ( D .- z ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) <-> ( ( D e. ( E I z ) /\ ( D .- z ) = ( B .- A ) ) /\ ( F e. ( E I t ) /\ ( F .- t ) = ( B .- C ) ) ) ) )
191 oveq2 
 |-  ( f = t -> ( z .- f ) = ( z .- t ) )
192 191 eqeq2d 
 |-  ( f = t -> ( ( x .- y ) = ( z .- f ) <-> ( x .- y ) = ( z .- t ) ) )
193 190 192 3anbi23d 
 |-  ( f = t -> ( ( ( ( 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 f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( z .- f ) ) <-> ( ( ( 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 ) ) ) )
194 184 193 cbvrex2vw 
 |-  ( E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) <-> E. z e. P E. 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 ) ) )
195 175 194 sylib 
 |-  ( ( ( ( ( ph /\ ( ( A =/= B /\ C =/= B ) /\ ( D =/= E /\ F =/= E ) ) ) /\ x e. P ) /\ y e. P ) /\ E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) ) -> E. z e. P E. 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 ) ) )
196 174 195 r19.29vva 
 |-  ( ( ( ( ( ph /\ ( ( A =/= B /\ C =/= B ) /\ ( D =/= E /\ F =/= E ) ) ) /\ x e. P ) /\ y e. P ) /\ E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
197 196 adantl3r 
 |-  ( ( ( ( ( ( ph /\ ( ( 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 ) ) ) /\ x e. P ) /\ y e. P ) /\ E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
198 simpr 
 |-  ( ( ( ph /\ ( ( 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 ) ) ) -> 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 ) ) )
199 oveq2 
 |-  ( a = x -> ( B I a ) = ( B I x ) )
200 199 eleq2d 
 |-  ( a = x -> ( A e. ( B I a ) <-> A e. ( B I x ) ) )
201 oveq2 
 |-  ( a = x -> ( A .- a ) = ( A .- x ) )
202 201 eqeq1d 
 |-  ( a = x -> ( ( A .- a ) = ( E .- D ) <-> ( A .- x ) = ( E .- D ) ) )
203 200 202 anbi12d 
 |-  ( a = x -> ( ( A e. ( B I a ) /\ ( A .- a ) = ( E .- D ) ) <-> ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) ) )
204 203 anbi1d 
 |-  ( a = x -> ( ( ( A e. ( B I a ) /\ ( A .- a ) = ( E .- D ) ) /\ ( C e. ( B I c ) /\ ( C .- c ) = ( E .- F ) ) ) <-> ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I c ) /\ ( C .- c ) = ( E .- F ) ) ) ) )
205 oveq1 
 |-  ( a = x -> ( a .- c ) = ( x .- c ) )
206 205 eqeq1d 
 |-  ( a = x -> ( ( a .- c ) = ( d .- f ) <-> ( x .- c ) = ( d .- f ) ) )
207 204 206 3anbi13d 
 |-  ( a = x -> ( ( ( ( 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 e. ( B I x ) /\ ( A .- x ) = ( 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 ) ) ) /\ ( x .- c ) = ( d .- f ) ) ) )
208 207 2rexbidv 
 |-  ( a = x -> ( 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 ) ) <-> E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( 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 ) ) ) /\ ( x .- c ) = ( d .- f ) ) ) )
209 oveq2 
 |-  ( c = y -> ( B I c ) = ( B I y ) )
210 209 eleq2d 
 |-  ( c = y -> ( C e. ( B I c ) <-> C e. ( B I y ) ) )
211 oveq2 
 |-  ( c = y -> ( C .- c ) = ( C .- y ) )
212 211 eqeq1d 
 |-  ( c = y -> ( ( C .- c ) = ( E .- F ) <-> ( C .- y ) = ( E .- F ) ) )
213 210 212 anbi12d 
 |-  ( c = y -> ( ( C e. ( B I c ) /\ ( C .- c ) = ( E .- F ) ) <-> ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) )
214 213 anbi2d 
 |-  ( c = y -> ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I c ) /\ ( C .- c ) = ( E .- F ) ) ) <-> ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) ) )
215 oveq2 
 |-  ( c = y -> ( x .- c ) = ( x .- y ) )
216 215 eqeq1d 
 |-  ( c = y -> ( ( x .- c ) = ( d .- f ) <-> ( x .- y ) = ( d .- f ) ) )
217 214 216 3anbi13d 
 |-  ( c = y -> ( ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( 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 ) ) ) /\ ( x .- c ) = ( d .- f ) ) <-> ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) ) )
218 217 2rexbidv 
 |-  ( c = y -> ( E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( 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 ) ) ) /\ ( x .- c ) = ( d .- f ) ) <-> E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) ) )
219 208 218 cbvrex2vw 
 |-  ( 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 ) ) <-> E. x e. P E. y e. P E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) )
220 198 219 sylib 
 |-  ( ( ( ph /\ ( ( 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 ) ) ) -> E. x e. P E. y e. P E. d e. P E. f e. P ( ( ( A e. ( B I x ) /\ ( A .- x ) = ( E .- D ) ) /\ ( C e. ( B I y ) /\ ( C .- y ) = ( E .- F ) ) ) /\ ( ( D e. ( E I d ) /\ ( D .- d ) = ( B .- A ) ) /\ ( F e. ( E I f ) /\ ( F .- f ) = ( B .- C ) ) ) /\ ( x .- y ) = ( d .- f ) ) )
221 197 220 r19.29vva 
 |-  ( ( ( ph /\ ( ( 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 "> ( cgrA ` G ) <" D E F "> )
222 221 anasss 
 |-  ( ( ph /\ ( ( ( 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 "> ( cgrA ` G ) <" D E F "> )
223 116 222 sylan2b 
 |-  ( ( ph /\ ( ( 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 "> ( cgrA ` G ) <" D E F "> )
224 115 223 impbida 
 |-  ( 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 ) ) ) ) )