Metamath Proof Explorer

Theorem hlpasch

Description: An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020)

Ref Expression
Hypotheses hlpasch.p 
|- P = ( Base ` G )
hlpasch.i 
|- I = ( Itv ` G )
hlpasch.k 
|- K = ( hlG ` G )
hlpasch.g 
|- ( ph -> G e. TarskiG )
hlpasch.1 
|- ( ph -> A e. P )
hlpasch.2 
|- ( ph -> B e. P )
hlpasch.3 
|- ( ph -> C e. P )
hlpasch.4 
|- ( ph -> X e. P )
hlpasch.5 
|- ( ph -> D e. P )
hlpasch.6 
|- ( ph -> A =/= B )
hlpasch.7 
|- ( ph -> C ( K ` B ) D )
hlpasch.8 
|- ( ph -> A e. ( X I C ) )
Assertion hlpasch 
|- ( ph -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )

Proof

Step Hyp Ref Expression
1 hlpasch.p 
 |-  P = ( Base ` G )
2 hlpasch.i 
 |-  I = ( Itv ` G )
3 hlpasch.k 
 |-  K = ( hlG ` G )
4 hlpasch.g 
 |-  ( ph -> G e. TarskiG )
5 hlpasch.1 
 |-  ( ph -> A e. P )
6 hlpasch.2 
 |-  ( ph -> B e. P )
7 hlpasch.3 
 |-  ( ph -> C e. P )
8 hlpasch.4 
 |-  ( ph -> X e. P )
9 hlpasch.5 
 |-  ( ph -> D e. P )
10 hlpasch.6 
 |-  ( ph -> A =/= B )
11 hlpasch.7 
 |-  ( ph -> C ( K ` B ) D )
12 hlpasch.8 
 |-  ( ph -> A e. ( X I C ) )
13 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
14 4 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> G e. TarskiG )
15 9 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> D e. P )
16 8 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> X e. P )
17 7 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> C e. P )
18 6 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> B e. P )
19 5 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> A e. P )
20 eqid 
 |-  ( dist ` G ) = ( dist ` G )
21 simpr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> C e. ( B I D ) )
22 1 20 2 14 18 17 15 21 tgbtwncom 
 |-  ( ( ph /\ C e. ( B I D ) ) -> C e. ( D I B ) )
23 12 adantr 
 |-  ( ( ph /\ C e. ( B I D ) ) -> A e. ( X I C ) )
24 1 2 13 14 15 16 17 18 19 22 23 outpasch 
 |-  ( ( ph /\ C e. ( B I D ) ) -> E. e e. P ( e e. ( D I X ) /\ A e. ( B I e ) ) )
25 simplr 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> e e. P )
26 18 ad2antrr 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> B e. P )
27 19 ad2antrr 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A e. P )
28 14 ad2antrr 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> G e. TarskiG )
29 simprr 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A e. ( B I e ) )
30 1 20 2 28 26 27 25 29 tgbtwncom 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A e. ( e I B ) )
31 28 adantr 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> G e. TarskiG )
32 26 adantr 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> B e. P )
33 27 adantr 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> A e. P )
34 simplrr 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> A e. ( B I e ) )
35 simpr 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> e = B )
36 35 oveq2d 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> ( B I e ) = ( B I B ) )
37 34 36 eleqtrd 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> A e. ( B I B ) )
38 1 20 2 31 32 33 37 axtgbtwnid 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> B = A )
39 38 eqcomd 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> A = B )
40 10 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A =/= B )
41 40 adantr 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> A =/= B )
42 41 neneqd 
 |-  ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> -. A = B )
43 39 42 pm2.65da 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> -. e = B )
44 43 neqned 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> e =/= B )
45 1 2 3 25 26 27 28 27 30 44 40 btwnhl2 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A ( K ` B ) e )
46 15 ad2antrr 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> D e. P )
47 16 ad2antrr 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> X e. P )
48 simprl 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> e e. ( D I X ) )
49 1 20 2 28 46 25 47 48 tgbtwncom 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> e e. ( X I D ) )
50 45 49 jca 
 |-  ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> ( A ( K ` B ) e /\ e e. ( X I D ) ) )
51 50 ex 
 |-  ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) -> ( ( e e. ( D I X ) /\ A e. ( B I e ) ) -> ( A ( K ` B ) e /\ e e. ( X I D ) ) ) )
52 51 reximdva 
 |-  ( ( ph /\ C e. ( B I D ) ) -> ( E. e e. P ( e e. ( D I X ) /\ A e. ( B I e ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) ) )
53 24 52 mpd 
 |-  ( ( ph /\ C e. ( B I D ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
54 9 ad2antrr 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) -> D e. P )
55 54 adantr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> D e. P )
56 simpr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) /\ e = D ) -> e = D )
57 56 breq2d 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) /\ e = D ) -> ( A ( K ` B ) e <-> A ( K ` B ) D ) )
58 56 eleq1d 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) /\ e = D ) -> ( e e. ( X I D ) <-> D e. ( X I D ) ) )
59 57 58 anbi12d 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) /\ e = D ) -> ( ( A ( K ` B ) e /\ e e. ( X I D ) ) <-> ( A ( K ` B ) D /\ D e. ( X I D ) ) ) )
60 5 ad2antrr 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) -> A e. P )
61 60 adantr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> A e. P )
62 6 ad2antrr 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) -> B e. P )
63 62 adantr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> B e. P )
64 4 ad2antrr 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) -> G e. TarskiG )
65 64 adantr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> G e. TarskiG )
66 1 2 3 7 9 6 4 11 hlcomd 
 |-  ( ph -> D ( K ` B ) C )
67 66 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> D ( K ` B ) C )
68 7 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> C e. P )
69 68 ad2antrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> C e. P )
70 12 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> A e. ( X I C ) )
71 70 ad2antrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> A e. ( X I C ) )
72 simpr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> X = B )
73 72 oveq1d 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> ( X I C ) = ( B I C ) )
74 71 73 eleqtrd 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> A e. ( B I C ) )
75 1 2 3 7 9 6 4 ishlg 
 |-  ( ph -> ( C ( K ` B ) D <-> ( C =/= B /\ D =/= B /\ ( C e. ( B I D ) \/ D e. ( B I C ) ) ) ) )
76 11 75 mpbid 
 |-  ( ph -> ( C =/= B /\ D =/= B /\ ( C e. ( B I D ) \/ D e. ( B I C ) ) ) )
77 76 simp1d 
 |-  ( ph -> C =/= B )
78 77 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> C =/= B )
79 10 ad2antrr 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) -> A =/= B )
80 79 adantr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> A =/= B )
81 1 2 3 55 69 63 65 61 74 78 80 hlbtwn 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> ( D ( K ` B ) C <-> D ( K ` B ) A ) )
82 67 81 mpbid 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> D ( K ` B ) A )
83 1 2 3 55 61 63 65 82 hlcomd 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> A ( K ` B ) D )
84 8 ad2antrr 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) -> X e. P )
85 84 adantr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> X e. P )
86 1 20 2 65 85 55 tgbtwntriv2 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> D e. ( X I D ) )
87 83 86 jca 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> ( A ( K ` B ) D /\ D e. ( X I D ) ) )
88 55 59 87 rspcedvd 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X = B ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
89 84 ad2antrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) -> X e. P )
90 simpr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ e = X ) -> e = X )
91 90 breq2d 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ e = X ) -> ( A ( K ` B ) e <-> A ( K ` B ) X ) )
92 90 eleq1d 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ e = X ) -> ( e e. ( X I D ) <-> X e. ( X I D ) ) )
93 91 92 anbi12d 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ e = X ) -> ( ( A ( K ` B ) e /\ e e. ( X I D ) ) <-> ( A ( K ` B ) X /\ X e. ( X I D ) ) ) )
94 93 ad4ant14 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) /\ e = X ) -> ( ( A ( K ` B ) e /\ e e. ( X I D ) ) <-> ( A ( K ` B ) X /\ X e. ( X I D ) ) ) )
95 simpr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) -> A ( K ` B ) X )
96 1 20 2 64 84 54 tgbtwntriv1 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) -> X e. ( X I D ) )
97 96 ad2antrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) -> X e. ( X I D ) )
98 95 97 jca 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) -> ( A ( K ` B ) X /\ X e. ( X I D ) ) )
99 89 94 98 rspcedvd 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
100 54 ad2antrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> D e. P )
101 simpr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) /\ e = D ) -> e = D )
102 101 breq2d 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) /\ e = D ) -> ( A ( K ` B ) e <-> A ( K ` B ) D ) )
103 101 eleq1d 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) /\ e = D ) -> ( e e. ( X I D ) <-> D e. ( X I D ) ) )
104 102 103 anbi12d 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) /\ e = D ) -> ( ( A ( K ` B ) e /\ e e. ( X I D ) ) <-> ( A ( K ` B ) D /\ D e. ( X I D ) ) ) )
105 79 ad2antrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A =/= B )
106 1 2 3 7 9 6 4 11 hlne2 
 |-  ( ph -> D =/= B )
107 106 ad4antr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> D =/= B )
108 64 ad2antrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> G e. TarskiG )
109 62 ad2antrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> B e. P )
110 60 ad2antrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A e. P )
111 68 ad2antrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> C e. P )
112 111 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> C e. P )
113 84 ad2antrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> X e. P )
114 simpr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> B e. ( X I A ) )
115 70 ad2antrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> A e. ( X I C ) )
116 115 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A e. ( X I C ) )
117 1 20 2 108 113 109 110 112 114 116 tgbtwnexch3 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A e. ( B I C ) )
118 simp-4r 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> D e. ( B I C ) )
119 1 2 108 109 110 100 112 117 118 tgbtwnconn3 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> ( A e. ( B I D ) \/ D e. ( B I A ) ) )
120 1 2 3 5 9 6 4 ishlg 
 |-  ( ph -> ( A ( K ` B ) D <-> ( A =/= B /\ D =/= B /\ ( A e. ( B I D ) \/ D e. ( B I A ) ) ) ) )
121 120 ad4antr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> ( A ( K ` B ) D <-> ( A =/= B /\ D =/= B /\ ( A e. ( B I D ) \/ D e. ( B I A ) ) ) ) )
122 105 107 119 121 mpbir3and 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A ( K ` B ) D )
123 1 20 2 108 113 100 tgbtwntriv2 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> D e. ( X I D ) )
124 122 123 jca 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> ( A ( K ` B ) D /\ D e. ( X I D ) ) )
125 100 104 124 rspcedvd 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
126 8 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> X e. P )
127 6 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> B e. P )
128 5 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> A e. P )
129 4 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> G e. TarskiG )
130 simpr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> X =/= B )
131 130 neneqd 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> -. X = B )
132 64 adantr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> G e. TarskiG )
133 132 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> G e. TarskiG )
134 126 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> X e. P )
135 128 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> A e. P )
136 115 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> A e. ( X I C ) )
137 simpr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> X = C )
138 137 oveq2d 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> ( X I X ) = ( X I C ) )
139 136 138 eleqtrrd 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> A e. ( X I X ) )
140 1 20 2 133 134 135 139 axtgbtwnid 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> X = A )
141 140 olcd 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> ( B e. ( X ( LineG ` G ) A ) \/ X = A ) )
142 132 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> G e. TarskiG )
143 127 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> B e. P )
144 111 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> C e. P )
145 126 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> X e. P )
146 128 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> A e. P )
147 simpr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> X =/= C )
148 147 necomd 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> C =/= X )
149 148 neneqd 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> -. C = X )
150 54 adantr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> D e. P )
151 106 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> D =/= B )
152 simplr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> X e. ( B ( LineG ` G ) D ) )
153 1 2 13 132 150 127 126 151 152 lncom 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> X e. ( D ( LineG ` G ) B ) )
154 77 necomd 
 |-  ( ph -> B =/= C )
155 154 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> B =/= C )
156 66 ad3antrrr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> D ( K ` B ) C )
157 1 2 3 150 111 127 132 13 156 hlln 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> D e. ( C ( LineG ` G ) B ) )
158 1 2 13 132 127 111 150 155 157 lncom 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> D e. ( B ( LineG ` G ) C ) )
159 158 orcd 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( D e. ( B ( LineG ` G ) C ) \/ B = C ) )
160 1 2 13 132 126 150 127 111 153 159 coltr 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( X e. ( B ( LineG ` G ) C ) \/ B = C ) )
161 1 13 2 132 127 111 126 160 colrot1 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( B e. ( C ( LineG ` G ) X ) \/ C = X ) )
162 161 orcomd 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( C = X \/ B e. ( C ( LineG ` G ) X ) ) )
163 162 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> ( C = X \/ B e. ( C ( LineG ` G ) X ) ) )
164 163 ord 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> ( -. C = X -> B e. ( C ( LineG ` G ) X ) ) )
165 149 164 mpd 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> B e. ( C ( LineG ` G ) X ) )
166 1 13 2 132 126 128 111 115 btwncolg3 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( C e. ( X ( LineG ` G ) A ) \/ X = A ) )
167 166 adantr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> ( C e. ( X ( LineG ` G ) A ) \/ X = A ) )
168 1 2 13 142 143 144 145 146 165 167 coltr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> ( B e. ( X ( LineG ` G ) A ) \/ X = A ) )
169 141 168 pm2.61dane 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( B e. ( X ( LineG ` G ) A ) \/ X = A ) )
170 1 13 2 132 126 128 127 169 colrot2 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( A e. ( B ( LineG ` G ) X ) \/ B = X ) )
171 1 13 2 132 127 126 128 170 colcom 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( A e. ( X ( LineG ` G ) B ) \/ X = B ) )
172 171 orcomd 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( X = B \/ A e. ( X ( LineG ` G ) B ) ) )
173 172 ord 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( -. X = B -> A e. ( X ( LineG ` G ) B ) ) )
174 131 173 mpd 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> A e. ( X ( LineG ` G ) B ) )
175 1 2 3 126 127 128 129 128 13 174 lnhl 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> ( A ( K ` B ) X \/ B e. ( X I A ) ) )
176 99 125 175 mpjaodan 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) /\ X =/= B ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
177 88 176 pm2.61dane 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B ( LineG ` G ) D ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
178 4 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> G e. TarskiG )
179 8 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> X e. P )
180 6 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> B e. P )
181 5 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> A e. P )
182 9 adantr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> D e. P )
183 simpr 
 |-  ( ( ph /\ D e. ( B I C ) ) -> D e. ( B I C ) )
184 1 20 2 178 179 180 68 181 182 70 183 axtgpasch 
 |-  ( ( ph /\ D e. ( B I C ) ) -> E. e e. P ( e e. ( A I B ) /\ e e. ( D I X ) ) )
185 184 adantr 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) -> E. e e. P ( e e. ( A I B ) /\ e e. ( D I X ) ) )
186 simplr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> e e. P )
187 181 ad3antrrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> A e. P )
188 180 ad3antrrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> B e. P )
189 178 ad3antrrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> G e. TarskiG )
190 simprl 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> e e. ( A I B ) )
191 1 20 2 189 187 186 188 190 tgbtwncom 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> e e. ( B I A ) )
192 10 necomd 
 |-  ( ph -> B =/= A )
193 192 ad4antr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> B =/= A )
194 189 adantr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> G e. TarskiG )
195 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> D e. P )
196 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> X e. P )
197 188 adantr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> B e. P )
198 simp-4r 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> -. X e. ( B ( LineG ` G ) D ) )
199 106 necomd 
 |-  ( ph -> B =/= D )
200 199 ad5antr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> B =/= D )
201 200 neneqd 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> -. B = D )
202 ioran 
 |-  ( -. ( X e. ( B ( LineG ` G ) D ) \/ B = D ) <-> ( -. X e. ( B ( LineG ` G ) D ) /\ -. B = D ) )
203 198 201 202 sylanbrc 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> -. ( X e. ( B ( LineG ` G ) D ) \/ B = D ) )
204 1 13 2 194 197 195 196 203 ncolrot2 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> -. ( D e. ( X ( LineG ` G ) B ) \/ X = B ) )
205 simpr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> e = B )
206 186 adantr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> e e. P )
207 1 2 13 194 195 196 197 204 ncolne1 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> D =/= X )
208 simplrr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> e e. ( D I X ) )
209 1 2 13 194 195 196 206 207 208 btwnlng1 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> e e. ( D ( LineG ` G ) X ) )
210 205 209 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> B e. ( D ( LineG ` G ) X ) )
211 1 2 13 194 195 196 207 tglinerflx1 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> D e. ( D ( LineG ` G ) X ) )
212 106 ad5antr 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> D =/= B )
213 212 necomd 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> B =/= D )
214 1 2 13 194 197 195 213 tglinerflx1 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> B e. ( B ( LineG ` G ) D ) )
215 1 2 13 194 197 195 213 tglinerflx2 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> D e. ( B ( LineG ` G ) D ) )
216 1 2 13 194 195 196 197 195 204 210 211 214 215 tglineinteq 
 |-  ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) /\ e = B ) -> B = D )
217 216 201 pm2.65da 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> -. e = B )
218 217 neqned 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> e =/= B )
219 1 2 3 188 187 186 189 187 191 193 218 btwnhl1 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> e ( K ` B ) A )
220 1 2 3 186 187 188 189 219 hlcomd 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> A ( K ` B ) e )
221 178 ad3antrrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> G e. TarskiG )
222 182 ad3antrrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> D e. P )
223 simplr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> e e. P )
224 179 ad3antrrr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> X e. P )
225 simpr 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> e e. ( D I X ) )
226 1 20 2 221 222 223 224 225 tgbtwncom 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> e e. ( X I D ) )
227 226 adantrl 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> e e. ( X I D ) )
228 220 227 jca 
 |-  ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) /\ ( e e. ( A I B ) /\ e e. ( D I X ) ) ) -> ( A ( K ` B ) e /\ e e. ( X I D ) ) )
229 228 ex 
 |-  ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) /\ e e. P ) -> ( ( e e. ( A I B ) /\ e e. ( D I X ) ) -> ( A ( K ` B ) e /\ e e. ( X I D ) ) ) )
230 229 reximdva 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) -> ( E. e e. P ( e e. ( A I B ) /\ e e. ( D I X ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) ) )
231 185 230 mpd 
 |-  ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B ( LineG ` G ) D ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
232 177 231 pm2.61dan 
 |-  ( ( ph /\ D e. ( B I C ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
233 76 simp3d 
 |-  ( ph -> ( C e. ( B I D ) \/ D e. ( B I C ) ) )
234 53 232 233 mpjaodan 
 |-  ( ph -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )