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

Theorem hlpasch 24877
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 2471 . . . 4  |-  (LineG `  G )  =  (LineG `  G )
4 hlpasch.g . . . . 5  |-  ( ph  ->  G  e. TarskiG )
54adantr 472 . . . 4  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  G  e. TarskiG )
6 hlpasch.5 . . . . 5  |-  ( ph  ->  D  e.  P )
76adantr 472 . . . 4  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  D  e.  P )
8 hlpasch.4 . . . . 5  |-  ( ph  ->  X  e.  P )
98adantr 472 . . . 4  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  X  e.  P )
10 hlpasch.3 . . . . 5  |-  ( ph  ->  C  e.  P )
1110adantr 472 . . . 4  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  C  e.  P )
12 hlpasch.2 . . . . 5  |-  ( ph  ->  B  e.  P )
1312adantr 472 . . . 4  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  B  e.  P )
14 hlpasch.1 . . . . 5  |-  ( ph  ->  A  e.  P )
1514adantr 472 . . . 4  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  A  e.  P )
16 eqid 2471 . . . . 5  |-  ( dist `  G )  =  (
dist `  G )
17 simpr 468 . . . . 5  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  C  e.  ( B I D ) )
181, 16, 2, 5, 13, 11, 7, 17tgbtwncom 24611 . . . 4  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  C  e.  ( D I B ) )
19 hlpasch.8 . . . . 5  |-  ( ph  ->  A  e.  ( X I C ) )
2019adantr 472 . . . 4  |-  ( (
ph  /\  C  e.  ( B I D ) )  ->  A  e.  ( X I C ) )
211, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20outpasch 24876 . . 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 770 . . . . . . 7  |-  ( ( ( ( ph  /\  C  e.  ( B I D ) )  /\  e  e.  P )  /\  ( e  e.  ( D I X )  /\  A  e.  ( B I e ) ) )  ->  e  e.  P )
2413ad2antrr 740 . . . . . . 7  |-  ( ( ( ( ph  /\  C  e.  ( B I D ) )  /\  e  e.  P )  /\  ( e  e.  ( D I X )  /\  A  e.  ( B I e ) ) )  ->  B  e.  P )
2515ad2antrr 740 . . . . . . 7  |-  ( ( ( ( ph  /\  C  e.  ( B I D ) )  /\  e  e.  P )  /\  ( e  e.  ( D I X )  /\  A  e.  ( B I e ) ) )  ->  A  e.  P )
265ad2antrr 740 . . . . . . 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 774 . . . . . . . 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 24611 . . . . . . 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 472 . . . . . . . . . . 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 472 . . . . . . . . . . 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 472 . . . . . . . . . . 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 472 . . . . . . . . . . . 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 468 . . . . . . . . . . . . 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 6324 . . . . . . . . . . . 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 2551 . . . . . . . . . . 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 24593 . . . . . . . . . 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 2477 . . . . . . . . 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 744 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  C  e.  ( B I D ) )  /\  e  e.  P )  /\  ( e  e.  ( D I X )  /\  A  e.  ( B I e ) ) )  ->  A  =/=  B )
4039adantr 472 . . . . . . . . . 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 2648 . . . . . . . . 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 586 . . . . . . . 8  |-  ( ( ( ( ph  /\  C  e.  ( B I D ) )  /\  e  e.  P )  /\  ( e  e.  ( D I X )  /\  A  e.  ( B I e ) ) )  ->  -.  e  =  B )
4342neqned 2650 . . . . . . 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 24737 . . . . . 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 740 . . . . . . 7  |-  ( ( ( ( ph  /\  C  e.  ( B I D ) )  /\  e  e.  P )  /\  ( e  e.  ( D I X )  /\  A  e.  ( B I e ) ) )  ->  D  e.  P )
469ad2antrr 740 . . . . . . 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 772 . . . . . . 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 24611 . . . . . 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 541 . . . . 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 441 . . . 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 2858 . . 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 740 . . . . . 6  |-  ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G ) D ) )  ->  D  e.  P )
5453adantr 472 . . . . 5  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  D  e.  P )
55 simpr 468 . . . . . . 7  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =  B )  /\  e  =  D )  ->  e  =  D )
5655breq2d 4407 . . . . . 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 2533 . . . . . 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 725 . . . . 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 740 . . . . . . . 8  |-  ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G ) D ) )  ->  A  e.  P )
6059adantr 472 . . . . . . 7  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  A  e.  P )
6112ad2antrr 740 . . . . . . . 8  |-  ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G ) D ) )  ->  B  e.  P )
6261adantr 472 . . . . . . 7  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  B  e.  P )
634ad2antrr 740 . . . . . . . 8  |-  ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G ) D ) )  ->  G  e. TarskiG )
6463adantr 472 . . . . . . 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 24728 . . . . . . . . 9  |-  ( ph  ->  D ( K `  B ) C )
6766ad3antrrr 744 . . . . . . . 8  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  D ( K `  B ) C )
6810adantr 472 . . . . . . . . . 10  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  C  e.  P )
6968ad2antrr 740 . . . . . . . . 9  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  C  e.  P )
7019adantr 472 . . . . . . . . . . 11  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  A  e.  ( X I C ) )
7170ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  A  e.  ( X I C ) )
72 simpr 468 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  X  =  B )
7372oveq1d 6323 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  ( X I C )  =  ( B I C ) )
7471, 73eleqtrd 2551 . . . . . . . . 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 24726 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ( K `
 B ) D  <-> 
( C  =/=  B  /\  D  =/=  B  /\  ( C  e.  ( B I D )  \/  D  e.  ( B I C ) ) ) ) )
7665, 75mpbid 215 . . . . . . . . . . 11  |-  ( ph  ->  ( C  =/=  B  /\  D  =/=  B  /\  ( C  e.  ( B I D )  \/  D  e.  ( B I C ) ) ) )
7776simp1d 1042 . . . . . . . . . 10  |-  ( ph  ->  C  =/=  B )
7877ad3antrrr 744 . . . . . . . . 9  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  C  =/=  B )
7938ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G ) D ) )  ->  A  =/=  B )
8079adantr 472 . . . . . . . . 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 24735 . . . . . . . 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 215 . . . . . . 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 24728 . . . . . 6  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  A ( K `  B ) D )
848ad2antrr 740 . . . . . . . 8  |-  ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G ) D ) )  ->  X  e.  P )
8584adantr 472 . . . . . . 7  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  X  e.  P )
861, 16, 2, 64, 85, 54tgbtwntriv2 24610 . . . . . 6  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =  B )  ->  D  e.  ( X I D ) )
8783, 86jca 541 . . . . 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 3143 . . . 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 740 . . . . . 6  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  A ( K `  B ) X )  ->  X  e.  P )
90 simpr 468 . . . . . . . . 9  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  e  =  X )  ->  e  =  X )
9190breq2d 4407 . . . . . . . 8  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  e  =  X )  ->  ( A ( K `
 B ) e  <-> 
A ( K `  B ) X ) )
9290eleq1d 2533 . . . . . . . 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 725 . . . . . . 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 1259 . . . . . 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 468 . . . . . . 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 24614 . . . . . . . 8  |-  ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G ) D ) )  ->  X  e.  ( X I D ) )
9796ad2antrr 740 . . . . . . 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 541 . . . . . 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 3143 . . . . 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 740 . . . . . 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 468 . . . . . . . 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 4407 . . . . . . 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 2533 . . . . . . 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 725 . . . . . 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 740 . . . . . . . . 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 24730 . . . . . . . . . 10  |-  ( ph  ->  D  =/=  B )
107106ad4antr 746 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  B  e.  ( X I A ) )  ->  D  =/=  B )
10863ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  B  e.  ( X I A ) )  ->  G  e. TarskiG )
10961ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  B  e.  ( X I A ) )  ->  B  e.  P )
11059ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  B  e.  ( X I A ) )  ->  A  e.  P )
11168ad2antrr 740 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  C  e.  P )
112111adantr 472 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  B  e.  ( X I A ) )  ->  C  e.  P )
11384ad2antrr 740 . . . . . . . . . . 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 468 . . . . . . . . . . 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 740 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  A  e.  ( X I C ) )
116115adantr 472 . . . . . . . . . . 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 24617 . . . . . . . . . 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 785 . . . . . . . . . 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 24701 . . . . . . . . 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 1210 . . . . . . . 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 24726 . . . . . . . . 9  |-  ( ph  ->  ( A ( K `
 B ) D  <-> 
( A  =/=  B  /\  D  =/=  B  /\  ( A  e.  ( B I D )  \/  D  e.  ( B I A ) ) ) ) )
122121ad4antr 746 . . . . . . . 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 240 . . . . . . 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 24610 . . . . . . 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 541 . . . . . 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 3143 . . . . 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 744 . . . . . 6  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  X  e.  P )
12812ad3antrrr 744 . . . . . 6  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  B  e.  P )
12914ad3antrrr 744 . . . . . 6  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  A  e.  P )
1304ad3antrrr 744 . . . . . 6  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  G  e. TarskiG )
131 simpr 468 . . . . . . . 8  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  X  =/=  B )
132131neneqd 2648 . . . . . . 7  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  -.  X  =  B
)
13363adantr 472 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  G  e. TarskiG )
134133adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =  C )  ->  G  e. TarskiG )
135127adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =  C )  ->  X  e.  P )
136129adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =  C )  ->  A  e.  P )
137115adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =  C )  ->  A  e.  ( X I C ) )
138 simpr 468 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =  C )  ->  X  =  C )
139138oveq2d 6324 . . . . . . . . . . . . . . 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 2552 . . . . . . . . . . . . . 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 24593 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =  C )  ->  X  =  A )
142141olcd 400 . . . . . . . . . . . 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 472 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =/=  C )  ->  G  e. TarskiG )
144128adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =/=  C )  ->  B  e.  P )
145111adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =/=  C )  ->  C  e.  P )
146127adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =/=  C )  ->  X  e.  P )
147129adantr 472 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =/=  C )  ->  A  e.  P )
148 simpr 468 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =/=  C )  ->  X  =/=  C )
149148necomd 2698 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =/=  C )  ->  C  =/=  X )
150149neneqd 2648 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B (LineG `  G
) D ) )  /\  X  =/=  B
)  /\  X  =/=  C )  ->  -.  C  =  X )
15153adantr 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  D  e.  P )
152106ad3antrrr 744 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  D  =/=  B )
153 simplr 770 . . . . . . . . . . . . . . . . . . . 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 24746 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  X  e.  ( D
(LineG `  G ) B ) )
15577necomd 2698 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  B  =/=  C )
156155ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  B  =/=  C )
15766ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . . 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 24731 . . . . . . . . . . . . . . . . . . . . 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 24746 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  ->  D  e.  ( B
(LineG `  G ) C ) )
160159orcd 399 . . . . . . . . . . . . . . . . . . 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 24771 . . . . . . . . . . . . . . . . . 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 24683 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  -> 
( B  e.  ( C (LineG `  G
) X )  \/  C  =  X ) )
163162orcomd 395 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  -> 
( C  =  X  \/  B  e.  ( C (LineG `  G
) X ) ) )
164163adantr 472 . . . . . . . . . . . . . . 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 384 . . . . . . . . . . . . . 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 24681 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  -> 
( C  e.  ( X (LineG `  G
) A )  \/  X  =  A ) )
168167adantr 472 . . . . . . . . . . . . 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 24771 . . . . . . . . . . . 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 2730 . . . . . . . . . . 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 24684 . . . . . . . . . 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 24682 . . . . . . . . 9  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  -> 
( A  e.  ( X (LineG `  G
) B )  \/  X  =  B ) )
173172orcomd 395 . . . . . . . 8  |-  ( ( ( ( ph  /\  D  e.  ( B I C ) )  /\  X  e.  ( B
(LineG `  G ) D ) )  /\  X  =/=  B )  -> 
( X  =  B  \/  A  e.  ( X (LineG `  G
) B ) ) )
174173ord 384 . . . . . . 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 24739 . . . . 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 803 . . . 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 2730 . . 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 472 . . . . . 6  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  G  e. TarskiG )
1808adantr 472 . . . . . 6  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  X  e.  P )
18112adantr 472 . . . . . 6  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  B  e.  P )
18214adantr 472 . . . . . 6  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  A  e.  P )
1836adantr 472 . . . . . 6  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  D  e.  P )
184 simpr 468 . . . . . 6  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  D  e.  ( B I C ) )
1851, 16, 2, 179, 180, 181, 68, 182, 183, 70, 184axtgpasch 24594 . . . . 5  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  E. e  e.  P  ( e  e.  ( A I B )  /\  e  e.  ( D I X ) ) )
186185adantr 472 . . . 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 770 . . . . . . . 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 744 . . . . . . . 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 744 . . . . . . . 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 744 . . . . . . . 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 772 . . . . . . . . . 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 24611 . . . . . . . . 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 2698 . . . . . . . . . 10  |-  ( ph  ->  B  =/=  A )
194193ad4antr 746 . . . . . . . . 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 472 . . . . . . . . . . . . 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 748 . . . . . . . . . . . . 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 748 . . . . . . . . . . . . 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 472 . . . . . . . . . . . . 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 785 . . . . . . . . . . . . . . . 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 2698 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  =/=  D )
201200ad5antr 748 . . . . . . . . . . . . . . . . 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 2648 . . . . . . . . . . . . . . . 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 541 . . . . . . . . . . . . . . 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 498 . . . . . . . . . . . . . . 15  |-  ( -.  ( X  e.  ( B (LineG `  G
) D )  \/  B  =  D )  <-> 
( -.  X  e.  ( B (LineG `  G ) D )  /\  -.  B  =  D ) )
205203, 204sylibr 217 . . . . . . . . . . . . . 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 24687 . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . 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 24749 . . . . . . . . . . . . . . 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 779 . . . . . . . . . . . . . . 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 24743 . . . . . . . . . . . . . 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 2550 . . . . . . . . . . . . 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 24674 . . . . . . . . . . . . . 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 24757 . . . . . . . . . . . . 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 748 . . . . . . . . . . . . . . 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 2698 . . . . . . . . . . . . . 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 24757 . . . . . . . . . . . . 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 24758 . . . . . . . . . . . . 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 24769 . . . . . . . . . . . 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 2477 . . . . . . . . . . 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 2648 . . . . . . . . . . 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 586 . . . . . . . . . 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 2650 . . . . . . . . 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 24736 . . . . . . . 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 24728 . . . . . . 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 744 . . . . . . . . 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 744 . . . . . . . . 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 770 . . . . . . . . 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 744 . . . . . . . . 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 468 . . . . . . . . 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 24611 . . . . . . . 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 730 . . . . . . 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 541 . . . . . 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 441 . . . . 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 2858 . . . 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 808 . 2  |-  ( (
ph  /\  D  e.  ( B I C ) )  ->  E. e  e.  P  ( A
( K `  B
) e  /\  e  e.  ( X I D ) ) )
23876simp3d 1044 . 2  |-  ( ph  ->  ( C  e.  ( B I D )  \/  D  e.  ( B I C ) ) )
23952, 237, 238mpjaodan 803 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 189    \/ wo 375    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904    =/= wne 2641   E.wrex 2757   class class class wbr 4395   ` cfv 5589  (class class class)co 6308   Basecbs 15199   distcds 15277  TarskiGcstrkg 24557  Itvcitv 24563  LineGclng 24564  hlGchlg 24724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-fzo 11943  df-hash 12554  df-word 12711  df-concat 12713  df-s1 12714  df-s2 13003  df-s3 13004  df-trkgc 24575  df-trkgb 24576  df-trkgcb 24577  df-trkgld 24579  df-trkg 24580  df-cgrg 24635  df-leg 24707  df-hlg 24725  df-mir 24777  df-rag 24818  df-perpg 24820
This theorem is referenced by:  inaghl  24960
  Copyright terms: Public domain W3C validator