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

Theorem tgbtwnconn1lem3 23018
Description: Lemma for tgbtwnconn1 23019 (Contributed by Thierry Arnoux, 30-Apr-2019.)
Hypotheses
Ref Expression
tgbtwnconn1.p  |-  P  =  ( Base `  G
)
tgbtwnconn1.i  |-  I  =  (Itv `  G )
tgbtwnconn1.g  |-  ( ph  ->  G  e. TarskiG )
tgbtwnconn1.a  |-  ( ph  ->  A  e.  P )
tgbtwnconn1.b  |-  ( ph  ->  B  e.  P )
tgbtwnconn1.c  |-  ( ph  ->  C  e.  P )
tgbtwnconn1.d  |-  ( ph  ->  D  e.  P )
tgbtwnconn1.1  |-  ( ph  ->  A  =/=  B )
tgbtwnconn1.2  |-  ( ph  ->  B  e.  ( A I C ) )
tgbtwnconn1.3  |-  ( ph  ->  B  e.  ( A I D ) )
tgbtwnconn1.m  |-  .-  =  ( dist `  G )
tgbtwnconn1.e  |-  ( ph  ->  E  e.  P )
tgbtwnconn1.f  |-  ( ph  ->  F  e.  P )
tgbtwnconn1.h  |-  ( ph  ->  H  e.  P )
tgbtwnconn1.j  |-  ( ph  ->  J  e.  P )
tgbtwnconn1.4  |-  ( ph  ->  D  e.  ( A I E ) )
tgbtwnconn1.5  |-  ( ph  ->  C  e.  ( A I F ) )
tgbtwnconn1.6  |-  ( ph  ->  E  e.  ( A I H ) )
tgbtwnconn1.7  |-  ( ph  ->  F  e.  ( A I J ) )
tgbtwnconn1.8  |-  ( ph  ->  ( E  .-  D
)  =  ( C 
.-  D ) )
tgbtwnconn1.9  |-  ( ph  ->  ( C  .-  F
)  =  ( C 
.-  D ) )
tgbtwnconn1.10  |-  ( ph  ->  ( E  .-  H
)  =  ( B 
.-  C ) )
tgbtwnconn1.11  |-  ( ph  ->  ( F  .-  J
)  =  ( B 
.-  D ) )
tgbtwnconn1.x  |-  ( ph  ->  X  e.  P )
tgbtwnconn1.12  |-  ( ph  ->  X  e.  ( C I E ) )
tgbtwnconn1.13  |-  ( ph  ->  X  e.  ( D I F ) )
tgbtwnconn1.14  |-  ( ph  ->  C  =/=  E )
Assertion
Ref Expression
tgbtwnconn1lem3  |-  ( ph  ->  D  =  F )

Proof of Theorem tgbtwnconn1lem3
Dummy variables  q  p  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tgbtwnconn1.p . . . . . 6  |-  P  =  ( Base `  G
)
2 tgbtwnconn1.m . . . . . 6  |-  .-  =  ( dist `  G )
3 tgbtwnconn1.i . . . . . 6  |-  I  =  (Itv `  G )
4 tgbtwnconn1.g . . . . . . . . 9  |-  ( ph  ->  G  e. TarskiG )
54ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  ->  G  e. TarskiG )
65ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C 
.-  p )  =  ( C  .-  F
) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  ->  G  e. TarskiG )
76ad2antrr 725 . . . . . 6  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  G  e. TarskiG )
8 tgbtwnconn1.f . . . . . . . 8  |-  ( ph  ->  F  e.  P )
98ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  ->  F  e.  P
)
109ad4antr 731 . . . . . 6  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  F  e.  P )
11 tgbtwnconn1.d . . . . . . 7  |-  ( ph  ->  D  e.  P )
1211ad6antr 735 . . . . . 6  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  D  e.  P )
13 simplr 754 . . . . . 6  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  q  e.  P )
147adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  G  e. TarskiG )
1512adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  D  e.  P )
1613adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  q  e.  P )
171, 2, 3, 14, 15, 16tgcgrtriv 22950 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( D  .-  D
)  =  ( q 
.-  q ) )
18 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  F  =  X )
19 tgbtwnconn1.x . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  P )
2019ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  ->  X  e.  P
)
2120ad4antr 731 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  X  e.  P )
2221adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  X  e.  P )
23 tgbtwnconn1.c . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  P )
24 tgbtwnconn1.e . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E  e.  P )
25 tgbtwnconn1.12 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  ( C I E ) )
26 eqidd 2444 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  .-  E
)  =  ( C 
.-  E ) )
27 eqidd 2444 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  .-  E
)  =  ( X 
.-  E ) )
28 tgbtwnconn1.9 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( C  .-  F
)  =  ( C 
.-  D ) )
2928eqcomd 2448 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  .-  D
)  =  ( C 
.-  F ) )
30 tgbtwnconn1.a . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  P )
31 tgbtwnconn1.b . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  P )
32 tgbtwnconn1.1 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  =/=  B )
33 tgbtwnconn1.2 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  ( A I C ) )
34 tgbtwnconn1.3 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  ( A I D ) )
35 tgbtwnconn1.h . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  H  e.  P )
36 tgbtwnconn1.j . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  J  e.  P )
37 tgbtwnconn1.4 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  D  e.  ( A I E ) )
38 tgbtwnconn1.5 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  C  e.  ( A I F ) )
39 tgbtwnconn1.6 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  e.  ( A I H ) )
40 tgbtwnconn1.7 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F  e.  ( A I J ) )
41 tgbtwnconn1.8 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E  .-  D
)  =  ( C 
.-  D ) )
42 tgbtwnconn1.10 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( E  .-  H
)  =  ( B 
.-  C ) )
43 tgbtwnconn1.11 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F  .-  J
)  =  ( B 
.-  D ) )
441, 3, 4, 30, 31, 23, 11, 32, 33, 34, 2, 24, 8, 35, 36, 37, 38, 39, 40, 41, 28, 42, 43tgbtwnconn1lem2 23017 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E  .-  F
)  =  ( C 
.-  D ) )
4541eqcomd 2448 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( C  .-  D
)  =  ( E 
.-  D ) )
4644, 45eqtr2d 2476 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( E  .-  D
)  =  ( E 
.-  F ) )
471, 2, 3, 4, 23, 19, 24, 11, 23, 19, 24, 8, 25, 25, 26, 27, 29, 46tgifscgr 22973 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( X  .-  D
)  =  ( X 
.-  F ) )
4847ad6antr 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( X  .-  D )  =  ( X  .-  F
) )
4948adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( X  .-  D
)  =  ( X 
.-  F ) )
5018oveq2d 6119 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( X  .-  F
)  =  ( X 
.-  X ) )
5149, 50eqtrd 2475 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( X  .-  D
)  =  ( X 
.-  X ) )
521, 2, 3, 14, 22, 15, 22, 51axtgcgrid 22936 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  X  =  D )
5318, 52eqtrd 2475 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  F  =  D )
5453oveq1d 6118 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( F  .-  D
)  =  ( D 
.-  D ) )
55 simp-4r 766 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C 
.-  p )  =  ( C  .-  F
) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  ->  p  e.  P )
5655ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  p  e.  P )
5756adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  p  e.  P )
58 simplr 754 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C 
.-  p )  =  ( C  .-  F
) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  ->  r  e.  P )
5958ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  r  e.  P )
6059adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  r  e.  P )
6110adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  F  e.  P )
6250eqcomd 2448 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( X  .-  X
)  =  ( X 
.-  F ) )
631, 2, 3, 14, 22, 22, 22, 61, 62tgcgrcomlr 22946 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( X  .-  X
)  =  ( F 
.-  X ) )
6423ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  ->  C  e.  P
)
6564ad4antr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  e.  P )
66 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  C  =  F )  ->  C  =  F )
674adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  C  =  F )  ->  G  e. TarskiG )
6824adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  C  =  F )  ->  E  e.  P )
698adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  C  =  F )  ->  F  e.  P )
7023adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  C  =  F )  ->  C  e.  P )
7166oveq2d 6119 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  C  =  F )  ->  ( C  .-  C )  =  ( C  .-  F
) )
7228, 44eqtr4d 2478 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( C  .-  F
)  =  ( E 
.-  F ) )
7372adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  C  =  F )  ->  ( C  .-  F )  =  ( E  .-  F
) )
7471, 73eqtr2d 2476 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  C  =  F )  ->  ( E  .-  F )  =  ( C  .-  C
) )
751, 2, 3, 67, 68, 69, 70, 74axtgcgrid 22936 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  C  =  F )  ->  E  =  F )
7666, 75eqtr4d 2478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  C  =  F )  ->  C  =  E )
77 tgbtwnconn1.14 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  C  =/=  E )
7877adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  C  =  F )  ->  C  =/=  E )
7978neneqd 2636 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  C  =  F )  ->  -.  C  =  E )
8076, 79pm2.65da 576 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  C  =  F )
8180neneqad 2693 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  C  =/=  F )
8281necomd 2707 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F  =/=  C )
8382ad6antr 735 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  F  =/=  C )
84 simpllr 758 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )
8584simpld 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  e.  ( F I r ) )
8624ad6antr 735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  E  e.  P )
871, 2, 3, 4, 23, 19, 24, 25tgbtwncom 22954 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  X  e.  ( E I C ) )
8887ad6antr 735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  X  e.  ( E I C ) )
89 simp-5r 768 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )
9089simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  e.  ( E I p ) )
911, 2, 3, 7, 86, 21, 65, 56, 88, 90tgbtwnexch3 22959 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  e.  ( X I p ) )
921, 2, 3, 7, 21, 65, 56, 91tgbtwncom 22954 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  e.  ( p I X ) )
9389simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  .-  p )  =  ( C  .-  F
) )
9493eqcomd 2448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  .-  F )  =  ( C  .-  p
) )
951, 2, 3, 7, 65, 10, 65, 56, 94tgcgrcomlr 22946 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( F  .-  C )  =  ( p  .-  C
) )
9684simprd 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  .-  r )  =  ( C  .-  X
) )
971, 2, 3, 7, 10, 56axtgcgrrflx 22935 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( F  .-  p )  =  ( p  .-  F
) )
981, 2, 3, 7, 10, 65, 59, 56, 65, 21, 56, 10, 83, 85, 92, 95, 96, 97, 93axtg5seg 22938 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  (
r  .-  p )  =  ( X  .-  F ) )
9998eqcomd 2448 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( X  .-  F )  =  ( r  .-  p
) )
1001, 2, 3, 7, 21, 10, 59, 56, 99tgcgrcomlr 22946 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( F  .-  X )  =  ( p  .-  r
) )
101100adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( F  .-  X
)  =  ( p 
.-  r ) )
10263, 101eqtr2d 2476 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( p  .-  r
)  =  ( X 
.-  X ) )
1031, 2, 3, 14, 57, 60, 22, 102axtgcgrid 22936 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  p  =  r )
104 simprr 756 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  (
r  .-  q )  =  ( r  .-  p ) )
105104adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( r  .-  q
)  =  ( r 
.-  p ) )
106103oveq2d 6119 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( r  .-  p
)  =  ( r 
.-  r ) )
107105, 106eqtrd 2475 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( r  .-  q
)  =  ( r 
.-  r ) )
1081, 2, 3, 14, 60, 16, 60, 107axtgcgrid 22936 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  r  =  q )
109103, 108eqtrd 2475 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  p  =  q )
110109oveq1d 6118 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( p  .-  q
)  =  ( q 
.-  q ) )
11117, 54, 1103eqtr4d 2485 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( F  .-  D
)  =  ( p 
.-  q ) )
1127adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  ->  G  e. TarskiG )
11310adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  ->  F  e.  P )
11421adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  ->  X  e.  P )
11512adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  ->  D  e.  P )
11656adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  ->  p  e.  P )
11759adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
r  e.  P )
11813adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
q  e.  P )
119 tgbtwnconn1.13 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  ( D I F ) )
1201, 2, 3, 4, 11, 19, 8, 119tgbtwncom 22954 . . . . . . . . . 10  |-  ( ph  ->  X  e.  ( F I D ) )
121120ad7antr 737 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  ->  X  e.  ( F I D ) )
122 simprl 755 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  r  e.  ( p I q ) )
123122adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
r  e.  ( p I q ) )
124100adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
( F  .-  X
)  =  ( p 
.-  r ) )
12598, 104, 483eqtr4d 2485 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  (
r  .-  q )  =  ( X  .-  D ) )
126125eqcomd 2448 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( X  .-  D )  =  ( r  .-  q
) )
127126adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
( X  .-  D
)  =  ( r 
.-  q ) )
1281, 2, 3, 112, 113, 114, 115, 116, 117, 118, 121, 123, 124, 127tgcgrextend 22951 . . . . . . . 8  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
( F  .-  D
)  =  ( p 
.-  q ) )
129111, 128pm2.61dane 2701 . . . . . . 7  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( F  .-  D )  =  ( p  .-  q
) )
130 eqid 2443 . . . . . . . . . . 11  |-  (LineG `  G )  =  (LineG `  G )
131 eqid 2443 . . . . . . . . . . 11  |-  (cgrG `  G )  =  (cgrG `  G )
13277ad6antr 735 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  =/=  E )
1331, 130, 3, 7, 65, 56, 86, 90btwncolg2 23002 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( E  e.  ( C
(LineG `  G )
p )  \/  C  =  p ) )
13428ad6antr 735 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  .-  F )  =  ( C  .-  D
) )
13595adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( F  .-  C
)  =  ( p 
.-  C ) )
13653oveq1d 6118 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( F  .-  C
)  =  ( D 
.-  C ) )
137109oveq1d 6118 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( p  .-  C
)  =  ( q 
.-  C ) )
138135, 136, 1373eqtr3d 2483 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =  X )  ->  ( D  .-  C
)  =  ( q 
.-  C ) )
13965adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  ->  C  e.  P )
140 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  ->  F  =/=  X )
14195adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
( F  .-  C
)  =  ( p 
.-  C ) )
14296eqcomd 2448 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  .-  X )  =  ( C  .-  r
) )
1431, 2, 3, 7, 65, 21, 65, 59, 142tgcgrcomlr 22946 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( X  .-  C )  =  ( r  .-  C
) )
144143adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
( X  .-  C
)  =  ( r 
.-  C ) )
1451, 2, 3, 112, 113, 114, 115, 116, 117, 118, 139, 139, 140, 121, 123, 124, 127, 141, 144axtg5seg 22938 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  F  =/=  X )  -> 
( D  .-  C
)  =  ( q 
.-  C ) )
146138, 145pm2.61dane 2701 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( D  .-  C )  =  ( q  .-  C
) )
1471, 2, 3, 7, 12, 65, 13, 65, 146tgcgrcomlr 22946 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  .-  D )  =  ( C  .-  q
) )
14893, 134, 1473eqtrd 2479 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( C  .-  p )  =  ( C  .-  q
) )
14931ad6antr 735 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  B  e.  P )
15036ad6antr 735 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  J  e.  P )
1517adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  G  e. TarskiG )
152150adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  J  e.  P )
15365adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  C  e.  P )
1541, 2, 3, 4, 30, 23, 8, 36, 38, 40tgbtwnexch3 22959 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  e.  ( C I J ) )
1551, 2, 3, 4, 30, 23, 8, 36, 81, 38, 154tgbtwnouttr 22962 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  C  e.  ( A I J ) )
1561, 2, 3, 4, 30, 31, 23, 36, 33, 155tgbtwnexch3 22959 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  C  e.  ( B I J ) )
157156ad7antr 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  C  e.  ( B I J ) )
158 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  B  =  J )
159158oveq1d 6118 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  ( B I J )  =  ( J I J ) )
160157, 159eleqtrd 2519 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  C  e.  ( J I J ) )
1611, 2, 3, 151, 152, 153, 160axtgbtwnid 22939 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  J  =  C )
16210adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  F  e.  P )
1631, 2, 3, 4, 31, 23, 8, 36, 156, 154tgbtwnexch2 22961 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F  e.  ( B I J ) )
164163ad7antr 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  F  e.  ( B I J ) )
165164, 159eleqtrd 2519 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  F  e.  ( J I J ) )
1661, 2, 3, 151, 152, 162, 165axtgbtwnid 22939 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  J  =  F )
167161, 166eqtr3d 2477 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  C  =  F )
16880ad7antr 737 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  B  =  J )  ->  -.  C  =  F )
169167, 168pm2.65da 576 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  -.  B  =  J )
170169neneqad 2693 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  B  =/=  J )
1711, 2, 3, 4, 30, 31, 11, 24, 34, 37tgbtwnexch 22963 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  ( A I E ) )
1721, 3, 4, 30, 31, 23, 11, 32, 33, 34, 2, 24, 8, 35, 36, 37, 38, 39, 40, 41, 28, 42, 43tgbtwnconn1lem1 23016 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  H  =  J )
173172oveq2d 6119 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A I H )  =  ( A I J ) )
17439, 173eleqtrd 2519 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  e.  ( A I J ) )
1751, 2, 3, 4, 30, 31, 24, 36, 171, 174tgbtwnexch3 22959 . . . . . . . . . . . . . 14  |-  ( ph  ->  E  e.  ( B I J ) )
176175ad6antr 735 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  E  e.  ( B I J ) )
1771, 130, 3, 7, 149, 86, 150, 176btwncolg3 23003 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( J  e.  ( B
(LineG `  G ) E )  \/  B  =  E ) )
17881ad6antr 735 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  =/=  F )
1791, 2, 3, 4, 8, 23, 31, 36, 154, 156tgbtwnintr 22958 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  ( F I B ) )
180179ad6antr 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  e.  ( F I B ) )
1811, 130, 3, 7, 65, 149, 10, 180btwncolg2 23002 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( F  e.  ( C
(LineG `  G ) B )  \/  C  =  B ) )
1827adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  G  e. TarskiG )
18365adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  C  e.  P )
18421adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  X  e.  P )
18559adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  r  e.  P )
18696adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  ( C  .-  r
)  =  ( C 
.-  X ) )
187 simpr 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  C  =  r )
188187oveq1d 6118 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  ( C  .-  r
)  =  ( r 
.-  r ) )
189186, 188eqtr3d 2477 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  ( C  .-  X
)  =  ( r 
.-  r ) )
1901, 2, 3, 182, 183, 184, 185, 189axtgcgrid 22936 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  C  =  X )
19186adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  E  e.  P )
192 eqidd 2444 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( D  .-  F
)  =  ( D 
.-  F ) )
193 eqidd 2444 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( X  .-  F
)  =  ( X 
.-  F ) )
1941, 2, 3, 4, 23, 11, 24, 11, 45tgcgrcomlr 22946 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( D  .-  C
)  =  ( D 
.-  E ) )
1951, 2, 3, 4, 23, 8, 24, 8, 72tgcgrcomlr 22946 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( F  .-  C
)  =  ( F 
.-  E ) )
1961, 2, 3, 4, 11, 19, 8, 23, 11, 19, 8, 24, 119, 119, 192, 193, 194, 195tgifscgr 22973 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( X  .-  C
)  =  ( X 
.-  E ) )
197196ad7antr 737 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  ( X  .-  C
)  =  ( X 
.-  E ) )
198190oveq2d 6119 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  ( X  .-  C
)  =  ( X 
.-  X ) )
199197, 198eqtr3d 2477 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  ( X  .-  E
)  =  ( X 
.-  X ) )
2001, 2, 3, 182, 184, 191, 184, 199axtgcgrid 22936 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  X  =  E )
201190, 200eqtrd 2475 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  C  =  E )
20277neneqd 2636 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  -.  C  =  E )
203202ad7antr 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P )  /\  ( C  e.  ( F I r )  /\  ( C  .-  r )  =  ( C  .-  X ) ) )  /\  q  e.  P
)  /\  ( r  e.  ( p I q )  /\  ( r 
.-  q )  =  ( r  .-  p
) ) )  /\  C  =  r )  ->  -.  C  =  E )
204201, 203pm2.65da 576 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  -.  C  =  r )
205204neneqad 2693 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  =/=  r )
2061, 2, 3, 7, 10, 65, 59, 85tgbtwncom 22954 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  C  e.  ( r I F ) )
2071, 130, 3, 7, 65, 10, 59, 206btwncolg2 23002 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  (
r  e.  ( C (LineG `  G ) F )  \/  C  =  F ) )
208104eqcomd 2448 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  (
r  .-  p )  =  ( r  .-  q ) )
2091, 130, 3, 7, 65, 59, 10, 131, 56, 13, 2, 205, 207, 148, 208lncgr 23013 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( F  .-  p )  =  ( F  .-  q
) )
2101, 130, 3, 7, 65, 10, 149, 131, 56, 13, 2, 178, 181, 148, 209lncgr 23013 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( B  .-  p )  =  ( B  .-  q
) )
211154ad6antr 735 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  F  e.  ( C I J ) )
2121, 130, 3, 7, 65, 150, 10, 211btwncolg1 23001 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( F  e.  ( C
(LineG `  G ) J )  \/  C  =  J ) )
2131, 130, 3, 7, 65, 10, 150, 131, 56, 13, 2, 178, 212, 148, 209lncgr 23013 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( J  .-  p )  =  ( J  .-  q
) )
2141, 130, 3, 7, 149, 150, 86, 131, 56, 13, 2, 170, 177, 210, 213lncgr 23013 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( E  .-  p )  =  ( E  .-  q
) )
2151, 130, 3, 7, 65, 86, 56, 131, 56, 13, 2, 132, 133, 148, 214lncgr 23013 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  (
p  .-  p )  =  ( p  .-  q ) )
216215eqcomd 2448 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  (
p  .-  q )  =  ( p  .-  p ) )
2171, 2, 3, 7, 56, 13, 56, 216axtgcgrid 22936 . . . . . . . 8  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  p  =  q )
218217oveq1d 6118 . . . . . . 7  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  (
p  .-  q )  =  ( q  .-  q ) )
219129, 218eqtrd 2475 . . . . . 6  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  ( F  .-  D )  =  ( q  .-  q
) )
2201, 2, 3, 7, 10, 12, 13, 219axtgcgrid 22936 . . . . 5  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  F  =  D )
221220eqcomd 2448 . . . 4  |-  ( ( ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C  .-  p )  =  ( C  .-  F ) ) )  /\  r  e.  P
)  /\  ( C  e.  ( F I r )  /\  ( C 
.-  r )  =  ( C  .-  X
) ) )  /\  q  e.  P )  /\  ( r  e.  ( p I q )  /\  ( r  .-  q )  =  ( r  .-  p ) ) )  ->  D  =  F )
2221, 2, 3, 6, 55, 58, 58, 55axtgsegcon 22937 . . . 4  |-  ( ( ( ( ( ph  /\  p  e.  P )  /\  ( C  e.  ( E I p )  /\  ( C 
.-  p )  =  ( C  .-  F
) ) )  /\  r  e.  P