Metamath Proof Explorer

Theorem tgbtwnconn1lem3

Description: Lemma for tgbtwnconn1 . (Contributed by Thierry Arnoux, 30-Apr-2019)

Ref Expression
Hypotheses 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 tgbtwnconn1lem3 
|- ( ph -> D = F )

Proof

Step Hyp Ref Expression
1 tgbtwnconn1.p 
 |-  P = ( Base ` G )
2 tgbtwnconn1.i 
 |-  I = ( Itv ` G )
3 tgbtwnconn1.g 
 |-  ( ph -> G e. TarskiG )
4 tgbtwnconn1.a 
 |-  ( ph -> A e. P )
5 tgbtwnconn1.b 
 |-  ( ph -> B e. P )
6 tgbtwnconn1.c 
 |-  ( ph -> C e. P )
7 tgbtwnconn1.d 
 |-  ( ph -> D e. P )
8 tgbtwnconn1.1 
 |-  ( ph -> A =/= B )
9 tgbtwnconn1.2 
 |-  ( ph -> B e. ( A I C ) )
10 tgbtwnconn1.3 
 |-  ( ph -> B e. ( A I D ) )
11 tgbtwnconn1.m 
 |-  .- = ( dist ` G )
12 tgbtwnconn1.e 
 |-  ( ph -> E e. P )
13 tgbtwnconn1.f 
 |-  ( ph -> F e. P )
14 tgbtwnconn1.h 
 |-  ( ph -> H e. P )
15 tgbtwnconn1.j 
 |-  ( ph -> J e. P )
16 tgbtwnconn1.4 
 |-  ( ph -> D e. ( A I E ) )
17 tgbtwnconn1.5 
 |-  ( ph -> C e. ( A I F ) )
18 tgbtwnconn1.6 
 |-  ( ph -> E e. ( A I H ) )
19 tgbtwnconn1.7 
 |-  ( ph -> F e. ( A I J ) )
20 tgbtwnconn1.8 
 |-  ( ph -> ( E .- D ) = ( C .- D ) )
21 tgbtwnconn1.9 
 |-  ( ph -> ( C .- F ) = ( C .- D ) )
22 tgbtwnconn1.10 
 |-  ( ph -> ( E .- H ) = ( B .- C ) )
23 tgbtwnconn1.11 
 |-  ( ph -> ( F .- J ) = ( B .- D ) )
24 tgbtwnconn1.x 
 |-  ( ph -> X e. P )
25 tgbtwnconn1.12 
 |-  ( ph -> X e. ( C I E ) )
26 tgbtwnconn1.13 
 |-  ( ph -> X e. ( D I F ) )
27 tgbtwnconn1.14 
 |-  ( ph -> C =/= E )
28 3 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
29 13 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
30 7 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
31 simplr 
 |-  ( ( ( ( ( ( ( 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 )
32 28 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
33 30 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
34 simpllr 
 |-  ( ( ( ( ( ( ( ( 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 )
35 1 11 2 32 33 34 tgcgrtriv 
 |-  ( ( ( ( ( ( ( ( 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 ) )
36 simpr 
 |-  ( ( ( ( ( ( ( ( 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 )
37 24 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
38 37 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
39 eqidd 
 |-  ( ph -> ( C .- E ) = ( C .- E ) )
40 eqidd 
 |-  ( ph -> ( X .- E ) = ( X .- E ) )
41 21 eqcomd 
 |-  ( ph -> ( C .- D ) = ( C .- F ) )
42 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 tgbtwnconn1lem2 
 |-  ( ph -> ( E .- F ) = ( C .- D ) )
43 20 42 eqtr4d 
 |-  ( ph -> ( E .- D ) = ( E .- F ) )
44 1 11 2 3 6 24 12 7 6 24 12 13 25 25 39 40 41 43 tgifscgr 
 |-  ( ph -> ( X .- D ) = ( X .- F ) )
45 44 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) )
46 45 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
47 36 oveq2d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
48 46 47 eqtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) )
49 1 11 2 32 38 33 38 48 axtgcgrid 
 |-  ( ( ( ( ( ( ( ( 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 )
50 36 49 eqtrd 
 |-  ( ( ( ( ( ( ( ( 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 )
51 50 oveq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
52 29 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
53 simp-4r 
 |-  ( ( ( ( ( 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 )
54 53 ad2antrr 
 |-  ( ( ( ( ( ( ( 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 )
55 54 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
56 simp-4r 
 |-  ( ( ( ( ( ( ( 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 )
57 56 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
58 6 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
59 simpr 
 |-  ( ( ph /\ C = F ) -> C = F )
60 3 adantr 
 |-  ( ( ph /\ C = F ) -> G e. TarskiG )
61 6 adantr 
 |-  ( ( ph /\ C = F ) -> C e. P )
62 13 adantr 
 |-  ( ( ph /\ C = F ) -> F e. P )
63 12 adantr 
 |-  ( ( ph /\ C = F ) -> E e. P )
64 21 42 eqtr4d 
 |-  ( ph -> ( C .- F ) = ( E .- F ) )
65 64 adantr 
 |-  ( ( ph /\ C = F ) -> ( C .- F ) = ( E .- F ) )
66 1 11 2 60 61 62 63 62 65 59 tgcgreq 
 |-  ( ( ph /\ C = F ) -> E = F )
67 59 66 eqtr4d 
 |-  ( ( ph /\ C = F ) -> C = E )
68 27 adantr 
 |-  ( ( ph /\ C = F ) -> C =/= E )
69 68 neneqd 
 |-  ( ( ph /\ C = F ) -> -. C = E )
70 67 69 pm2.65da 
 |-  ( ph -> -. C = F )
71 70 neqned 
 |-  ( ph -> C =/= F )
72 71 necomd 
 |-  ( ph -> F =/= C )
73 72 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
74 simpllr 
 |-  ( ( ( ( ( ( ( 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 ) ) )
75 74 simpld 
 |-  ( ( ( ( ( ( ( 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 ) )
76 12 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
77 1 11 2 3 6 24 12 25 tgbtwncom 
 |-  ( ph -> X e. ( E I C ) )
78 77 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) )
79 simp-5r 
 |-  ( ( ( ( ( ( ( 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 ) ) )
80 79 simpld 
 |-  ( ( ( ( ( ( ( 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 ) )
81 1 11 2 28 76 37 58 54 78 80 tgbtwnexch3 
 |-  ( ( ( ( ( ( ( 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 ) )
82 1 11 2 28 37 58 54 81 tgbtwncom 
 |-  ( ( ( ( ( ( ( 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 ) )
83 79 simprd 
 |-  ( ( ( ( ( ( ( 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 ) )
84 83 eqcomd 
 |-  ( ( ( ( ( ( ( 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 ) )
85 1 11 2 28 58 29 58 54 84 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( 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 ) )
86 74 simprd 
 |-  ( ( ( ( ( ( ( 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 ) )
87 1 11 2 28 29 54 axtgcgrrflx 
 |-  ( ( ( ( ( ( ( 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 ) )
88 1 11 2 28 29 58 56 54 58 37 54 29 73 75 82 85 86 87 83 axtg5seg 
 |-  ( ( ( ( ( ( ( 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 ) )
89 88 eqcomd 
 |-  ( ( ( ( ( ( ( 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 ) )
90 1 11 2 28 37 29 56 54 89 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( 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 ) )
91 90 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
92 1 11 2 32 52 38 55 57 91 36 tgcgreq 
 |-  ( ( ( ( ( ( ( ( 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 )
93 simprr 
 |-  ( ( ( ( ( ( ( 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 ) )
94 93 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
95 92 oveq2d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
96 94 95 eqtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) )
97 1 11 2 32 57 34 57 96 axtgcgrid 
 |-  ( ( ( ( ( ( ( ( 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 )
98 92 97 eqtrd 
 |-  ( ( ( ( ( ( ( ( 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 )
99 98 oveq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
100 35 51 99 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
101 28 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
102 29 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
103 37 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
104 30 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
105 54 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
106 56 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
107 simpllr 
 |-  ( ( ( ( ( ( ( ( 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 )
108 1 11 2 3 7 24 13 26 tgbtwncom 
 |-  ( ph -> X e. ( F I D ) )
109 108 ad7antr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
110 simplrl 
 |-  ( ( ( ( ( ( ( ( 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 ) )
111 90 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
112 88 93 45 3eqtr4rd 
 |-  ( ( ( ( ( ( ( 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 ) )
113 112 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
114 1 11 2 101 102 103 104 105 106 107 109 110 111 113 tgcgrextend 
 |-  ( ( ( ( ( ( ( ( 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 ) )
115 100 114 pm2.61dane 
 |-  ( ( ( ( ( ( ( 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 ) )
116 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
117 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
118 27 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
119 1 116 2 28 58 54 76 80 btwncolg2 
 |-  ( ( ( ( ( ( ( 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 ) )
120 21 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) )
121 85 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
122 50 oveq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
123 98 oveq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
124 121 122 123 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
125 58 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
126 simpr 
 |-  ( ( ( ( ( ( ( ( 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 )
127 85 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
128 86 eqcomd 
 |-  ( ( ( ( ( ( ( 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 ) )
129 1 11 2 28 58 37 58 56 128 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( 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 ) )
130 129 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
131 1 11 2 101 102 103 104 105 106 107 125 125 126 109 110 111 113 127 130 axtg5seg 
 |-  ( ( ( ( ( ( ( ( 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 ) )
132 124 131 pm2.61dane 
 |-  ( ( ( ( ( ( ( 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 ) )
133 1 11 2 28 30 58 31 58 132 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( 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 ) )
134 83 120 133 3eqtrd 
 |-  ( ( ( ( ( ( ( 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 ) )
135 5 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
136 15 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
137 28 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
138 136 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
139 58 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
140 1 11 2 3 4 6 13 15 17 19 tgbtwnexch 
 |-  ( ph -> C e. ( A I J ) )
141 1 11 2 3 4 5 6 15 9 140 tgbtwnexch3 
 |-  ( ph -> C e. ( B I J ) )
142 141 ad7antr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
143 simpr 
 |-  ( ( ( ( ( ( ( ( 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 )
144 143 oveq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
145 142 144 eleqtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) )
146 1 11 2 137 138 139 145 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ( 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 )
147 29 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
148 1 11 2 3 4 6 13 15 17 19 tgbtwnexch3 
 |-  ( ph -> F e. ( C I J ) )
149 1 11 2 3 5 6 13 15 141 148 tgbtwnexch2 
 |-  ( ph -> F e. ( B I J ) )
150 149 ad7antr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
151 150 144 eleqtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) )
152 1 11 2 137 138 147 151 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ( 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 )
153 146 152 eqtr3d 
 |-  ( ( ( ( ( ( ( ( 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 )
154 70 ad7antr 
 |-  ( ( ( ( ( ( ( ( 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 )
155 153 154 pm2.65da 
 |-  ( ( ( ( ( ( ( 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 )
156 155 neqned 
 |-  ( ( ( ( ( ( ( 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 )
157 1 11 2 3 4 5 7 12 10 16 tgbtwnexch 
 |-  ( ph -> B e. ( A I E ) )
158 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 tgbtwnconn1lem1 
 |-  ( ph -> H = J )
159 158 oveq2d 
 |-  ( ph -> ( A I H ) = ( A I J ) )
160 18 159 eleqtrd 
 |-  ( ph -> E e. ( A I J ) )
161 1 11 2 3 4 5 12 15 157 160 tgbtwnexch3 
 |-  ( ph -> E e. ( B I J ) )
162 161 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) )
163 1 116 2 28 135 76 136 162 btwncolg3 
 |-  ( ( ( ( ( ( ( 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 ) )
164 71 ad6antr 
 |-  ( ( ( ( ( ( ( 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 )
165 1 11 2 3 13 6 5 15 148 141 tgbtwnintr 
 |-  ( ph -> C e. ( F I B ) )
166 165 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) )
167 1 116 2 28 58 135 29 166 btwncolg2 
 |-  ( ( ( ( ( ( ( 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 ) )
168 28 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
169 58 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
170 56 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
171 37 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
172 86 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
173 simpr 
 |-  ( ( ( ( ( ( ( ( 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 )
174 1 11 2 168 169 170 169 171 172 173 tgcgreq 
 |-  ( ( ( ( ( ( ( ( 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 )
175 76 adantr 
 |-  ( ( ( ( ( ( ( ( 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 )
176 eqidd 
 |-  ( ph -> ( D .- F ) = ( D .- F ) )
177 eqidd 
 |-  ( ph -> ( X .- F ) = ( X .- F ) )
178 20 eqcomd 
 |-  ( ph -> ( C .- D ) = ( E .- D ) )
179 1 11 2 3 6 7 12 7 178 tgcgrcomlr 
 |-  ( ph -> ( D .- C ) = ( D .- E ) )
180 1 11 2 3 6 13 12 13 64 tgcgrcomlr 
 |-  ( ph -> ( F .- C ) = ( F .- E ) )
181 1 11 2 3 7 24 13 6 7 24 13 12 26 26 176 177 179 180 tgifscgr 
 |-  ( ph -> ( X .- C ) = ( X .- E ) )
182 181 ad7antr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
183 174 oveq2d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
184 182 183 eqtr3d 
 |-  ( ( ( ( ( ( ( ( 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 ) )
185 1 11 2 168 171 175 171 184 axtgcgrid 
 |-  ( ( ( ( ( ( ( ( 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 )
186 174 185 eqtrd 
 |-  ( ( ( ( ( ( ( ( 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 )
187 27 neneqd 
 |-  ( ph -> -. C = E )
188 187 ad7antr 
 |-  ( ( ( ( ( ( ( ( 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 )
189 186 188 pm2.65da 
 |-  ( ( ( ( ( ( ( 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 )
190 189 neqned 
 |-  ( ( ( ( ( ( ( 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 )
191 1 11 2 28 29 58 56 75 tgbtwncom 
 |-  ( ( ( ( ( ( ( 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 ) )
192 1 116 2 28 58 29 56 191 btwncolg2 
 |-  ( ( ( ( ( ( ( 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 ) )
193 93 eqcomd 
 |-  ( ( ( ( ( ( ( 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 ) )
194 1 116 2 28 58 56 29 117 54 31 11 190 192 134 193 lncgr 
 |-  ( ( ( ( ( ( ( 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 ) )
195 1 116 2 28 58 29 135 117 54 31 11 164 167 134 194 lncgr 
 |-  ( ( ( ( ( ( ( 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 ) )
196 148 ad6antr 
 |-  ( ( ( ( ( ( ( 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 ) )
197 1 116 2 28 58 136 29 196 btwncolg1 
 |-  ( ( ( ( ( ( ( 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 ) )
198 1 116 2 28 58 29 136 117 54 31 11 164 197 134 194 lncgr 
 |-  ( ( ( ( ( ( ( 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 ) )
199 1 116 2 28 135 136 76 117 54 31 11 156 163 195 198 lncgr 
 |-  ( ( ( ( ( ( ( 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 ) )
200 1 116 2 28 58 76 54 117 31 58 11 118 119 134 199 lnid 
 |-  ( ( ( ( ( ( ( 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 )
201 200 oveq1d 
 |-  ( ( ( ( ( ( ( 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 ) )
202 115 201 eqtrd 
 |-  ( ( ( ( ( ( ( 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 ) )
203 1 11 2 28 29 30 31 202 axtgcgrid 
 |-  ( ( ( ( ( ( ( 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 )
204 203 eqcomd 
 |-  ( ( ( ( ( ( ( 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 )
205 3 ad2antrr 
 |-  ( ( ( ph /\ p e. P ) /\ ( C e. ( E I p ) /\ ( C .- p ) = ( C .- F ) ) ) -> G e. TarskiG )
206 205 ad2antrr 
 |-  ( ( ( ( ( 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 )
207 simplr 
 |-  ( ( ( ( ( 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 )
208 1 11 2 206 53 207 207 53 axtgsegcon 
 |-  ( ( ( ( ( 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 ) ) ) -> E. q e. P ( r e. ( p I q ) /\ ( r .- q ) = ( r .- p ) ) )
209 204 208 r19.29a 
 |-  ( ( ( ( ( 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 ) ) ) -> D = F )
210 13 ad2antrr 
 |-  ( ( ( ph /\ p e. P ) /\ ( C e. ( E I p ) /\ ( C .- p ) = ( C .- F ) ) ) -> F e. P )
211 6 ad2antrr 
 |-  ( ( ( ph /\ p e. P ) /\ ( C e. ( E I p ) /\ ( C .- p ) = ( C .- F ) ) ) -> C e. P )
212 24 ad2antrr 
 |-  ( ( ( ph /\ p e. P ) /\ ( C e. ( E I p ) /\ ( C .- p ) = ( C .- F ) ) ) -> X e. P )
213 1 11 2 205 210 211 211 212 axtgsegcon 
 |-  ( ( ( ph /\ p e. P ) /\ ( C e. ( E I p ) /\ ( C .- p ) = ( C .- F ) ) ) -> E. r e. P ( C e. ( F I r ) /\ ( C .- r ) = ( C .- X ) ) )
214 209 213 r19.29a 
 |-  ( ( ( ph /\ p e. P ) /\ ( C e. ( E I p ) /\ ( C .- p ) = ( C .- F ) ) ) -> D = F )
215 1 11 2 3 12 6 6 13 axtgsegcon 
 |-  ( ph -> E. p e. P ( C e. ( E I p ) /\ ( C .- p ) = ( C .- F ) ) )
216 214 215 r19.29a 
 |-  ( ph -> D = F )