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 ) ) )