MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hlpasch Structured version   Visualization version   Unicode version
Theorem hlpasch 25648
Description: An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020.)
Hypotheses
Ref Expression
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
Ref Expression
hlpasch |- ( ph -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
Distinct variable groups:   A, e   B, e   C, e   D, e   e, G   e, I   e, K   P, e   e, X   ph, e
Proof of Theorem hlpasch
StepHypRef Expression
1 hlpasch.p . . . 4 |- P = ( Base ` G )
2 hlpasch.i . . . 4 |- I = (Itv ` G )
3 eqid 2622 . . . 4 |- (LineG ` G ) = (LineG ` G )
4 hlpasch.g . . . . 5 |- ( ph -> G e. TarskiG )
54adantr 481 . . . 4 |- ( ( ph /\ C e. ( B I D ) ) -> G e. TarskiG )
6 hlpasch.5 . . . . 5 |- ( ph -> D e. P )
76adantr 481 . . . 4 |- ( ( ph /\ C e. ( B I D ) ) -> D e. P )
8 hlpasch.4 . . . . 5 |- ( ph -> X e. P )
98adantr 481 . . . 4 |- ( ( ph /\ C e. ( B I D ) ) -> X e. P )
10 hlpasch.3 . . . . 5 |- ( ph -> C e. P )
1110adantr 481 . . . 4 |- ( ( ph /\ C e. ( B I D ) ) -> C e. P )
12 hlpasch.2 . . . . 5 |- ( ph -> B e. P )
1312adantr 481 . . . 4 |- ( ( ph /\ C e. ( B I D ) ) -> B e. P )
14 hlpasch.1 . . . . 5 |- ( ph -> A e. P )
1514adantr 481 . . . 4 |- ( ( ph /\ C e. ( B I D ) ) -> A e. P )
16 eqid 2622 . . . . 5 |- ( dist ` G ) = ( dist ` G )
17 simpr 477 . . . . 5 |- ( ( ph /\ C e. ( B I D ) ) -> C e. ( B I D ) )
181, 16, 2, 5, 13, 11, 7, 17tgbtwncom 25383 . . . 4 |- ( ( ph /\ C e. ( B I D ) ) -> C e. ( D I B ) )
19 hlpasch.8 . . . . 5 |- ( ph -> A e. ( X I C ) )
2019adantr 481 . . . 4 |- ( ( ph /\ C e. ( B I D ) ) -> A e. ( X I C ) )
211, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20outpasch 25647 . . 3 |- ( ( ph /\ C e. ( B I D ) ) -> E. e e. P ( e e. ( D I X ) /\ A e. ( B I e ) ) )
22 hlpasch.k . . . . . . 7 |- K = (hlG ` G )
23 simplr 792 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> e e. P )
2413ad2antrr 762 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> B e. P )
2515ad2antrr 762 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A e. P )
265ad2antrr 762 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> G e. TarskiG )
27 simprr 796 . . . . . . . 8 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A e. ( B I e ) )
281, 16, 2, 26, 24, 25, 23, 27tgbtwncom 25383 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A e. ( e I B ) )
2926adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> G e. TarskiG )
3024adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> B e. P )
3125adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> A e. P )
3227adantr 481 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
33 simpr 477 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> e = B )
3433oveq2d 6666 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
3532, 34eleqtrd 2703 . . . . . . . . . . 11 |- ( ( ( ( ( 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 ) )
361, 16, 2, 29, 30, 31, 35axtgbtwnid 25365 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> B = A )
3736eqcomd 2628 . . . . . . . . 9 |- ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> A = B )
38 hlpasch.6 . . . . . . . . . . . 12 |- ( ph -> A =/= B )
3938ad3antrrr 766 . . . . . . . . . . 11 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A =/= B )
4039adantr 481 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> A =/= B )
4140neneqd 2799 . . . . . . . . 9 |- ( ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) /\ e = B ) -> -. A = B )
4237, 41pm2.65da 600 . . . . . . . 8 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> -. e = B )
4342neqned 2801 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> e =/= B )
441, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39btwnhl2 25508 . . . . . 6 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> A ( K ` B ) e )
457ad2antrr 762 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> D e. P )
469ad2antrr 762 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> X e. P )
47 simprl 794 . . . . . . 7 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> e e. ( D I X ) )
481, 16, 2, 26, 45, 23, 46, 47tgbtwncom 25383 . . . . . 6 |- ( ( ( ( ph /\ C e. ( B I D ) ) /\ e e. P ) /\ ( e e. ( D I X ) /\ A e. ( B I e ) ) ) -> e e. ( X I D ) )
4944, 48jca 554 . . . . 5 |- ( ( ( ( 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 ) ) )
5049ex 450 . . . 4 |- ( ( ( 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 ) ) ) )
5150reximdva 3017 . . 3 |- ( ( 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 ) ) ) )
5221, 51mpd 15 . 2 |- ( ( ph /\ C e. ( B I D ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
536ad2antrr 762 . . . . . 6 |- ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) -> D e. P )
5453adantr 481 . . . . 5 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> D e. P )
55 simpr 477 . . . . . . 7 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) /\ e = D ) -> e = D )
5655breq2d 4665 . . . . . 6 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) /\ e = D ) -> ( A ( K ` B ) e <-> A ( K ` B ) D ) )
5755eleq1d 2686 . . . . . 6 |- ( ( ( ( ( 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 ) ) )
5856, 57anbi12d 747 . . . . 5 |- ( ( ( ( ( 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 ) ) ) )
5914ad2antrr 762 . . . . . . . 8 |- ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) -> A e. P )
6059adantr 481 . . . . . . 7 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> A e. P )
6112ad2antrr 762 . . . . . . . 8 |- ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) -> B e. P )
6261adantr 481 . . . . . . 7 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> B e. P )
634ad2antrr 762 . . . . . . . 8 |- ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) -> G e. TarskiG )
6463adantr 481 . . . . . . 7 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> G e. TarskiG )
65 hlpasch.7 . . . . . . . . . 10 |- ( ph -> C ( K ` B ) D )
661, 2, 22, 10, 6, 12, 4, 65hlcomd 25499 . . . . . . . . 9 |- ( ph -> D ( K ` B ) C )
6766ad3antrrr 766 . . . . . . . 8 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> D ( K ` B ) C )
6810adantr 481 . . . . . . . . . 10 |- ( ( ph /\ D e. ( B I C ) ) -> C e. P )
6968ad2antrr 762 . . . . . . . . 9 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> C e. P )
7019adantr 481 . . . . . . . . . . 11 |- ( ( ph /\ D e. ( B I C ) ) -> A e. ( X I C ) )
7170ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> A e. ( X I C ) )
72 simpr 477 . . . . . . . . . . 11 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> X = B )
7372oveq1d 6665 . . . . . . . . . 10 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> ( X I C ) = ( B I C ) )
7471, 73eleqtrd 2703 . . . . . . . . 9 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> A e. ( B I C ) )
751, 2, 22, 10, 6, 12, 4ishlg 25497 . . . . . . . . . . . 12 |- ( ph -> ( C ( K ` B ) D <-> ( C =/= B /\ D =/= B /\ ( C e. ( B I D ) \/ D e. ( B I C ) ) ) ) )
7665, 75mpbid 222 . . . . . . . . . . 11 |- ( ph -> ( C =/= B /\ D =/= B /\ ( C e. ( B I D ) \/ D e. ( B I C ) ) ) )
7776simp1d 1073 . . . . . . . . . 10 |- ( ph -> C =/= B )
7877ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> C =/= B )
7938ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) -> A =/= B )
8079adantr 481 . . . . . . . . 9 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> A =/= B )
811, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80hlbtwn 25506 . . . . . . . 8 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> ( D ( K ` B ) C <-> D ( K ` B ) A ) )
8267, 81mpbid 222 . . . . . . 7 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> D ( K ` B ) A )
831, 2, 22, 54, 60, 62, 64, 82hlcomd 25499 . . . . . 6 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> A ( K ` B ) D )
848ad2antrr 762 . . . . . . . 8 |- ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) -> X e. P )
8584adantr 481 . . . . . . 7 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> X e. P )
861, 16, 2, 64, 85, 54tgbtwntriv2 25382 . . . . . 6 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> D e. ( X I D ) )
8783, 86jca 554 . . . . 5 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X = B ) -> ( A ( K ` B ) D /\ D e. ( X I D ) ) )
8854, 58, 87rspcedvd 3317 . . . 4 |- ( ( ( ( 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 ) ) )
8984ad2antrr 762 . . . . . 6 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) -> X e. P )
90 simpr 477 . . . . . . . . 9 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ e = X ) -> e = X )
9190breq2d 4665 . . . . . . . 8 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ e = X ) -> ( A ( K ` B ) e <-> A ( K ` B ) X ) )
9290eleq1d 2686 . . . . . . . 8 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ e = X ) -> ( e e. ( X I D ) <-> X e. ( X I D ) ) )
9391, 92anbi12d 747 . . . . . . 7 |- ( ( ( ( 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 ) ) ) )
9493ad4ant14 1293 . . . . . 6 |- ( ( ( ( ( ( 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 477 . . . . . . 7 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) -> A ( K ` B ) X )
961, 16, 2, 63, 84, 53tgbtwntriv1 25386 . . . . . . . 8 |- ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) -> X e. ( X I D ) )
9796ad2antrr 762 . . . . . . 7 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ A ( K ` B ) X ) -> X e. ( X I D ) )
9895, 97jca 554 . . . . . 6 |- ( ( ( ( ( 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 ) ) )
9989, 94, 98rspcedvd 3317 . . . . 5 |- ( ( ( ( ( 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 ) ) )
10053ad2antrr 762 . . . . . 6 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> D e. P )
101 simpr 477 . . . . . . . 8 |- ( ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) /\ e = D ) -> e = D )
102101breq2d 4665 . . . . . . 7 |- ( ( ( ( ( ( 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 ) )
103101eleq1d 2686 . . . . . . 7 |- ( ( ( ( ( ( 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 ) ) )
104102, 103anbi12d 747 . . . . . 6 |- ( ( ( ( ( ( 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 ) ) ) )
10579ad2antrr 762 . . . . . . . . 9 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A =/= B )
1061, 2, 22, 10, 6, 12, 4, 65hlne2 25501 . . . . . . . . . 10 |- ( ph -> D =/= B )
107106ad4antr 768 . . . . . . . . 9 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> D =/= B )
10863ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> G e. TarskiG )
10961ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> B e. P )
11059ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A e. P )
11168ad2antrr 762 . . . . . . . . . . 11 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> C e. P )
112111adantr 481 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> C e. P )
11384ad2antrr 762 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> X e. P )
114 simpr 477 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> B e. ( X I A ) )
11570ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> A e. ( X I C ) )
116115adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A e. ( X I C ) )
1171, 16, 2, 108, 113, 109, 110, 112, 114, 116tgbtwnexch3 25389 . . . . . . . . . 10 |- ( ( ( ( ( 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 807 . . . . . . . . . 10 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> D e. ( B I C ) )
1191, 2, 108, 109, 110, 100, 112, 117, 118tgbtwnconn3 25472 . . . . . . . . 9 |- ( ( ( ( ( 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 ) ) )
120105, 107, 1193jca 1242 . . . . . . . 8 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> ( A =/= B /\ D =/= B /\ ( A e. ( B I D ) \/ D e. ( B I A ) ) ) )
1211, 2, 22, 14, 6, 12, 4ishlg 25497 . . . . . . . . 9 |- ( ph -> ( A ( K ` B ) D <-> ( A =/= B /\ D =/= B /\ ( A e. ( B I D ) \/ D e. ( B I A ) ) ) ) )
122121ad4antr 768 . . . . . . . 8 |- ( ( ( ( ( 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 ) ) ) ) )
123120, 122mpbird 247 . . . . . . 7 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> A ( K ` B ) D )
1241, 16, 2, 108, 113, 100tgbtwntriv2 25382 . . . . . . 7 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ B e. ( X I A ) ) -> D e. ( X I D ) )
125123, 124jca 554 . . . . . 6 |- ( ( ( ( ( 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 ) ) )
126100, 104, 125rspcedvd 3317 . . . . 5 |- ( ( ( ( ( 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 ) ) )
1278ad3antrrr 766 . . . . . 6 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> X e. P )
12812ad3antrrr 766 . . . . . 6 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> B e. P )
12914ad3antrrr 766 . . . . . 6 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> A e. P )
1304ad3antrrr 766 . . . . . 6 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> G e. TarskiG )
131 simpr 477 . . . . . . . 8 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> X =/= B )
132131neneqd 2799 . . . . . . 7 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> -. X = B )
13363adantr 481 . . . . . . . . . 10 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> G e. TarskiG )
134133adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> G e. TarskiG )
135127adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> X e. P )
136129adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> A e. P )
137115adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> A e. ( X I C ) )
138 simpr 477 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> X = C )
139138oveq2d 6666 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> ( X I X ) = ( X I C ) )
140137, 139eleqtrrd 2704 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> A e. ( X I X ) )
1411, 16, 2, 134, 135, 136, 140axtgbtwnid 25365 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> X = A )
142141olcd 408 . . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X = C ) -> ( B e. ( X (LineG ` G ) A ) \/ X = A ) )
143133adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> G e. TarskiG )
144128adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> B e. P )
145111adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> C e. P )
146127adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> X e. P )
147129adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> A e. P )
148 simpr 477 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> X =/= C )
149148necomd 2849 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> C =/= X )
150149neneqd 2799 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> -. C = X )
15153adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> D e. P )
152106ad3antrrr 766 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> D =/= B )
153 simplr 792 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> X e. ( B (LineG ` G ) D ) )
1541, 2, 3, 133, 151, 128, 127, 152, 153lncom 25517 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> X e. ( D (LineG ` G ) B ) )
15577necomd 2849 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> B =/= C )
156155ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> B =/= C )
15766ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> D ( K ` B ) C )
1581, 2, 22, 151, 111, 128, 133, 3, 157hlln 25502 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> D e. ( C (LineG ` G ) B ) )
1591, 2, 3, 133, 128, 111, 151, 156, 158lncom 25517 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> D e. ( B (LineG ` G ) C ) )
160159orcd 407 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( D e. ( B (LineG ` G ) C ) \/ B = C ) )
1611, 2, 3, 133, 127, 151, 128, 111, 154, 160coltr 25542 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( X e. ( B (LineG ` G ) C ) \/ B = C ) )
1621, 3, 2, 133, 128, 111, 127, 161colrot1 25454 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( B e. ( C (LineG ` G ) X ) \/ C = X ) )
163162orcomd 403 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( C = X \/ B e. ( C (LineG ` G ) X ) ) )
164163adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> ( C = X \/ B e. ( C (LineG ` G ) X ) ) )
165164ord 392 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> ( -. C = X -> B e. ( C (LineG ` G ) X ) ) )
166150, 165mpd 15 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> B e. ( C (LineG ` G ) X ) )
1671, 3, 2, 133, 127, 129, 111, 115btwncolg3 25452 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( C e. ( X (LineG ` G ) A ) \/ X = A ) )
168167adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> ( C e. ( X (LineG ` G ) A ) \/ X = A ) )
1691, 2, 3, 143, 144, 145, 146, 147, 166, 168coltr 25542 . . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) /\ X =/= C ) -> ( B e. ( X (LineG ` G ) A ) \/ X = A ) )
170142, 169pm2.61dane 2881 . . . . . . . . . . 11 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( B e. ( X (LineG ` G ) A ) \/ X = A ) )
1711, 3, 2, 133, 127, 129, 128, 170colrot2 25455 . . . . . . . . . 10 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( A e. ( B (LineG ` G ) X ) \/ B = X ) )
1721, 3, 2, 133, 128, 127, 129, 171colcom 25453 . . . . . . . . 9 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( A e. ( X (LineG ` G ) B ) \/ X = B ) )
173172orcomd 403 . . . . . . . 8 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( X = B \/ A e. ( X (LineG ` G ) B ) ) )
174173ord 392 . . . . . . 7 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( -. X = B -> A e. ( X (LineG ` G ) B ) ) )
175132, 174mpd 15 . . . . . 6 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> A e. ( X (LineG ` G ) B ) )
1761, 2, 22, 127, 128, 129, 130, 129, 3, 175lnhl 25510 . . . . 5 |- ( ( ( ( ph /\ D e. ( B I C ) ) /\ X e. ( B (LineG ` G ) D ) ) /\ X =/= B ) -> ( A ( K ` B ) X \/ B e. ( X I A ) ) )
17799, 126, 176mpjaodan 827 . . . 4 |- ( ( ( ( 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 ) ) )
17888, 177pm2.61dane 2881 . . 3 |- ( ( ( 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 ) ) )
1794adantr 481 . . . . . 6 |- ( ( ph /\ D e. ( B I C ) ) -> G e. TarskiG )
1808adantr 481 . . . . . 6 |- ( ( ph /\ D e. ( B I C ) ) -> X e. P )
18112adantr 481 . . . . . 6 |- ( ( ph /\ D e. ( B I C ) ) -> B e. P )
18214adantr 481 . . . . . 6 |- ( ( ph /\ D e. ( B I C ) ) -> A e. P )
1836adantr 481 . . . . . 6 |- ( ( ph /\ D e. ( B I C ) ) -> D e. P )
184 simpr 477 . . . . . 6 |- ( ( ph /\ D e. ( B I C ) ) -> D e. ( B I C ) )
1851, 16, 2, 179, 180, 181, 68, 182, 183, 70, 184axtgpasch 25366 . . . . 5 |- ( ( ph /\ D e. ( B I C ) ) -> E. e e. P ( e e. ( A I B ) /\ e e. ( D I X ) ) )
186185adantr 481 . . . 4 |- ( ( ( 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 ) ) )
187 simplr 792 . . . . . . . 8 |- ( ( ( ( ( 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 )
188182ad3antrrr 766 . . . . . . . 8 |- ( ( ( ( ( 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 )
189181ad3antrrr 766 . . . . . . . 8 |- ( ( ( ( ( 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 )
190179ad3antrrr 766 . . . . . . . 8 |- ( ( ( ( ( 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 )
191 simprl 794 . . . . . . . . . 10 |- ( ( ( ( ( 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 ) )
1921, 16, 2, 190, 188, 187, 189, 191tgbtwncom 25383 . . . . . . . . 9 |- ( ( ( ( ( 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 ) )
19338necomd 2849 . . . . . . . . . 10 |- ( ph -> B =/= A )
194193ad4antr 768 . . . . . . . . 9 |- ( ( ( ( ( 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 )
195190adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 )
1966ad5antr 770 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 )
1978ad5antr 770 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 )
198189adantr 481 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 )
199 simp-4r 807 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) )
200106necomd 2849 . . . . . . . . . . . . . . . . . 18 |- ( ph -> B =/= D )
201200ad5antr 770 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
202201neneqd 2799 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 )
203199, 202jca 554 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 ioran 511 . . . . . . . . . . . . . . 15 |- ( -. ( X e. ( B (LineG ` G ) D ) \/ B = D ) <-> ( -. X e. ( B (LineG ` G ) D ) /\ -. B = D ) )
205203, 204sylibr 224 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) )
2061, 3, 2, 195, 198, 196, 197, 205ncolrot2 25458 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
207 simpr 477 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
208187adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
2091, 2, 3, 195, 196, 197, 198, 206ncolne1 25520 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
210 simplrr 801 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 ) )
2111, 2, 3, 195, 196, 197, 208, 209, 210btwnlng1 25514 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) )
212207, 211eqeltrrd 2702 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
2131, 3, 2, 195, 196, 197, 212tglngne 25445 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
2141, 2, 3, 195, 196, 197, 213tglinerflx1 25528 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
215106ad5antr 770 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
216215necomd 2849 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
2171, 2, 3, 195, 198, 196, 216tglinerflx1 25528 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
2181, 2, 3, 195, 198, 196, 216tglinerflx2 25529 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
2191, 2, 3, 195, 196, 197, 198, 196, 206, 212, 214, 217, 218tglineinteq 25540 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
220219eqcomd 2628 . . . . . . . . . . 11 |- ( ( ( ( ( ( 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 )
221215neneqd 2799 . . . . . . . . . . 11 |- ( ( ( ( ( ( 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 )
222220, 221pm2.65da 600 . . . . . . . . . 10 |- ( ( ( ( ( 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 )
223222neqned 2801 . . . . . . . . 9 |- ( ( ( ( ( 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 )
2241, 2, 22, 189, 188, 187, 190, 188, 192, 194, 223btwnhl1 25507 . . . . . . . 8 |- ( ( ( ( ( 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 )
2251, 2, 22, 187, 188, 189, 190, 224hlcomd 25499 . . . . . . 7 |- ( ( ( ( ( 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 )
226179ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B (LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> G e. TarskiG )
227183ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B (LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> D e. P )
228 simplr 792 . . . . . . . . 9 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B (LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> e e. P )
229180ad3antrrr 766 . . . . . . . . 9 |- ( ( ( ( ( ph /\ D e. ( B I C ) ) /\ -. X e. ( B (LineG ` G ) D ) ) /\ e e. P ) /\ e e. ( D I X ) ) -> X e. P )
230 simpr 477 . . . . . . . . 9 |- ( ( ( ( ( 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 ) )
2311, 16, 2, 226, 227, 228, 229, 230tgbtwncom 25383 . . . . . . . 8 |- ( ( ( ( ( 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 ) )
232231adantrl 752 . . . . . . 7 |- ( ( ( ( ( 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 ) )
233225, 232jca 554 . . . . . 6 |- ( ( ( ( ( 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 ) ) )
234233ex 450 . . . . 5 |- ( ( ( ( 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 ) ) ) )
235234reximdva 3017 . . . 4 |- ( ( ( 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 ) ) ) )
236186, 235mpd 15 . . 3 |- ( ( ( 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 ) ) )
237178, 236pm2.61dan 832 . 2 |- ( ( ph /\ D e. ( B I C ) ) -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
23876simp3d 1075 . 2 |- ( ph -> ( C e. ( B I D ) \/ D e. ( B I C ) ) )
23952, 237, 238mpjaodan 827 1 |- ( ph -> E. e e. P ( A ( K ` B ) e /\ e e. ( X I D ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  Itvcitv 25335  LineGclng 25336  hlGchlg 25495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-hash 13118  df-word 13299  df-concat 13301  df-s1 13302  df-s2 13593  df-s3 13594  df-trkgc 25347  df-trkgb 25348  df-trkgcb 25349  df-trkgld 25351  df-trkg 25352  df-cgrg 25406  df-leg 25478  df-hlg 25496  df-mir 25548  df-rag 25589  df-perpg 25591
This theorem is referenced by:  inaghl  25731
  Copyright terms: Public domain W3C validator