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

Theorem acopyeu 24923
Description: Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points  X and  Y both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-Aug-2020.)
Hypotheses
Ref Expression
dfcgra2.p  |-  P  =  ( Base `  G
)
dfcgra2.i  |-  I  =  (Itv `  G )
dfcgra2.m  |-  .-  =  ( dist `  G )
dfcgra2.g  |-  ( ph  ->  G  e. TarskiG )
dfcgra2.a  |-  ( ph  ->  A  e.  P )
dfcgra2.b  |-  ( ph  ->  B  e.  P )
dfcgra2.c  |-  ( ph  ->  C  e.  P )
dfcgra2.d  |-  ( ph  ->  D  e.  P )
dfcgra2.e  |-  ( ph  ->  E  e.  P )
dfcgra2.f  |-  ( ph  ->  F  e.  P )
acopy.l  |-  L  =  (LineG `  G )
acopy.1  |-  ( ph  ->  -.  ( A  e.  ( B L C )  \/  B  =  C ) )
acopy.2  |-  ( ph  ->  -.  ( D  e.  ( E L F )  \/  E  =  F ) )
acopyeu.x  |-  ( ph  ->  X  e.  P )
acopyeu.y  |-  ( ph  ->  Y  e.  P )
acopyeu.k  |-  K  =  (hlG `  G )
acopyeu.1  |-  ( ph  ->  <" A B C "> (cgrA `  G ) <" D E X "> )
acopyeu.2  |-  ( ph  ->  <" A B C "> (cgrA `  G ) <" D E Y "> )
acopyeu.3  |-  ( ph  ->  X ( (hpG `  G ) `  ( D L E ) ) F )
acopyeu.4  |-  ( ph  ->  Y ( (hpG `  G ) `  ( D L E ) ) F )
Assertion
Ref Expression
acopyeu  |-  ( ph  ->  X ( K `  E ) Y )

Proof of Theorem acopyeu
Dummy variables  a 
d  t  x  y  b  u  v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfcgra2.p . . . 4  |-  P  =  ( Base `  G
)
2 dfcgra2.i . . . 4  |-  I  =  (Itv `  G )
3 acopyeu.k . . . 4  |-  K  =  (hlG `  G )
4 acopyeu.x . . . . . 6  |-  ( ph  ->  X  e.  P )
54ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  X  e.  P
)
65ad3antrrr 741 . . . 4  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  X  e.  P )
7 simplr 767 . . . 4  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  y  e.  P )
8 acopyeu.y . . . . . 6  |-  ( ph  ->  Y  e.  P )
98ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  Y  e.  P
)
109ad3antrrr 741 . . . 4  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  Y  e.  P )
11 dfcgra2.g . . . . . 6  |-  ( ph  ->  G  e. TarskiG )
1211ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  G  e. TarskiG )
1312ad3antrrr 741 . . . 4  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  G  e. TarskiG )
14 dfcgra2.e . . . . . 6  |-  ( ph  ->  E  e.  P )
1514ad2antrr 737 . . . . 5  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  E  e.  P
)
1615ad3antrrr 741 . . . 4  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  E  e.  P )
17 dfcgra2.m . . . . . . 7  |-  .-  =  ( dist `  G )
18 acopy.l . . . . . . 7  |-  L  =  (LineG `  G )
19 dfcgra2.a . . . . . . . . 9  |-  ( ph  ->  A  e.  P )
2019ad2antrr 737 . . . . . . . 8  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  A  e.  P
)
2120ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  A  e.  P )
22 dfcgra2.b . . . . . . . . 9  |-  ( ph  ->  B  e.  P )
2322ad2antrr 737 . . . . . . . 8  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  B  e.  P
)
2423ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  B  e.  P )
25 dfcgra2.c . . . . . . . . 9  |-  ( ph  ->  C  e.  P )
2625ad2antrr 737 . . . . . . . 8  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  C  e.  P
)
2726ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  C  e.  P )
28 simplr 767 . . . . . . . 8  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  d  e.  P
)
2928ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  d  e.  P )
30 dfcgra2.f . . . . . . . . 9  |-  ( ph  ->  F  e.  P )
3130ad2antrr 737 . . . . . . . 8  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  F  e.  P
)
3231ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  F  e.  P )
33 acopy.1 . . . . . . . . 9  |-  ( ph  ->  -.  ( A  e.  ( B L C )  \/  B  =  C ) )
3433ad2antrr 737 . . . . . . . 8  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  -.  ( A  e.  ( B L C )  \/  B  =  C ) )
3534ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  ( A  e.  ( B L C )  \/  B  =  C ) )
36 dfcgra2.d . . . . . . . . . 10  |-  ( ph  ->  D  e.  P )
3736ad2antrr 737 . . . . . . . . 9  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  D  e.  P
)
38 acopy.2 . . . . . . . . . 10  |-  ( ph  ->  -.  ( D  e.  ( E L F )  \/  E  =  F ) )
3938ad2antrr 737 . . . . . . . . 9  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  -.  ( D  e.  ( E L F )  \/  E  =  F ) )
40 simprl 769 . . . . . . . . . 10  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  d ( K `
 E ) D )
411, 2, 3, 28, 37, 15, 12, 18, 40hlln 24700 . . . . . . . . 9  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  d  e.  ( D L E ) )
421, 2, 3, 28, 37, 15, 12, 40hlne1 24698 . . . . . . . . 9  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  d  =/=  E
)
431, 2, 18, 12, 37, 15, 31, 28, 39, 41, 42ncolncol 24739 . . . . . . . 8  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  -.  ( d  e.  ( E L F )  \/  E  =  F ) )
4443ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  ( d  e.  ( E L F )  \/  E  =  F ) )
45 simprr 771 . . . . . . . . . 10  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( E  .-  d )  =  ( B  .-  A ) )
461, 17, 2, 12, 15, 28, 23, 20, 45tgcgrcomlr 24572 . . . . . . . . 9  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( d  .-  E )  =  ( A  .-  B ) )
4746eqcomd 2467 . . . . . . . 8  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( A  .-  B )  =  ( d  .-  E ) )
4847ad3antrrr 741 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  ( A  .-  B )  =  ( d  .-  E
) )
49 simpl 463 . . . . . . . . . . 11  |-  ( ( u  =  a  /\  v  =  b )  ->  u  =  a )
5049eleq1d 2523 . . . . . . . . . 10  |-  ( ( u  =  a  /\  v  =  b )  ->  ( u  e.  ( P  \  ( d L E ) )  <-> 
a  e.  ( P 
\  ( d L E ) ) ) )
51 simpr 467 . . . . . . . . . . 11  |-  ( ( u  =  a  /\  v  =  b )  ->  v  =  b )
5251eleq1d 2523 . . . . . . . . . 10  |-  ( ( u  =  a  /\  v  =  b )  ->  ( v  e.  ( P  \  ( d L E ) )  <-> 
b  e.  ( P 
\  ( d L E ) ) ) )
5350, 52anbi12d 722 . . . . . . . . 9  |-  ( ( u  =  a  /\  v  =  b )  ->  ( ( u  e.  ( P  \  (
d L E ) )  /\  v  e.  ( P  \  (
d L E ) ) )  <->  ( a  e.  ( P  \  (
d L E ) )  /\  b  e.  ( P  \  (
d L E ) ) ) ) )
54 simpr 467 . . . . . . . . . . 11  |-  ( ( ( u  =  a  /\  v  =  b )  /\  w  =  t )  ->  w  =  t )
55 simpll 765 . . . . . . . . . . . 12  |-  ( ( ( u  =  a  /\  v  =  b )  /\  w  =  t )  ->  u  =  a )
56 simplr 767 . . . . . . . . . . . 12  |-  ( ( ( u  =  a  /\  v  =  b )  /\  w  =  t )  ->  v  =  b )
5755, 56oveq12d 6332 . . . . . . . . . . 11  |-  ( ( ( u  =  a  /\  v  =  b )  /\  w  =  t )  ->  (
u I v )  =  ( a I b ) )
5854, 57eleq12d 2533 . . . . . . . . . 10  |-  ( ( ( u  =  a  /\  v  =  b )  /\  w  =  t )  ->  (
w  e.  ( u I v )  <->  t  e.  ( a I b ) ) )
5958cbvrexdva 3037 . . . . . . . . 9  |-  ( ( u  =  a  /\  v  =  b )  ->  ( E. w  e.  ( d L E ) w  e.  ( u I v )  <->  E. t  e.  (
d L E ) t  e.  ( a I b ) ) )
6053, 59anbi12d 722 . . . . . . . 8  |-  ( ( u  =  a  /\  v  =  b )  ->  ( ( ( u  e.  ( P  \ 
( d L E ) )  /\  v  e.  ( P  \  (
d L E ) ) )  /\  E. w  e.  ( d L E ) w  e.  ( u I v ) )  <->  ( (
a  e.  ( P 
\  ( d L E ) )  /\  b  e.  ( P  \  ( d L E ) ) )  /\  E. t  e.  ( d L E ) t  e.  ( a I b ) ) ) )
6160cbvopabv 4485 . . . . . . 7  |-  { <. u ,  v >.  |  ( ( u  e.  ( P  \  ( d L E ) )  /\  v  e.  ( P  \  ( d L E ) ) )  /\  E. w  e.  ( d L E ) w  e.  ( u I v ) ) }  =  { <. a ,  b >.  |  ( ( a  e.  ( P  \ 
( d L E ) )  /\  b  e.  ( P  \  (
d L E ) ) )  /\  E. t  e.  ( d L E ) t  e.  ( a I b ) ) }
62 simpllr 774 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  x  e.  P )
63 simprll 777 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  <" A B C "> (cgrG `  G ) <" d E x "> )
64 simprrl 779 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  <" A B C "> (cgrG `  G ) <" d E y "> )
651, 2, 18, 11, 36, 14, 30, 38ncolne1 24718 . . . . . . . . . . . . 13  |-  ( ph  ->  D  =/=  E )
661, 2, 18, 11, 36, 14, 65tgelrnln 24723 . . . . . . . . . . . 12  |-  ( ph  ->  ( D L E )  e.  ran  L
)
6766ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( D L E )  e.  ran  L )
681, 2, 18, 11, 36, 14, 65tglinerflx2 24727 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  ( D L E ) )
6968ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  E  e.  ( D L E ) )
701, 2, 18, 12, 28, 15, 42, 42, 67, 41, 69tglinethru 24729 . . . . . . . . . 10  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( D L E )  =  ( d L E ) )
7170, 67eqeltrrd 2540 . . . . . . . . 9  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( d L E )  e.  ran  L )
7271ad3antrrr 741 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  (
d L E )  e.  ran  L )
7361eqcomi 2470 . . . . . . . 8  |-  { <. a ,  b >.  |  ( ( a  e.  ( P  \  ( d L E ) )  /\  b  e.  ( P  \  ( d L E ) ) )  /\  E. t  e.  ( d L E ) t  e.  ( a I b ) ) }  =  { <. u ,  v >.  |  ( ( u  e.  ( P  \ 
( d L E ) )  /\  v  e.  ( P  \  (
d L E ) ) )  /\  E. w  e.  ( d L E ) w  e.  ( u I v ) ) }
7469, 70eleqtrd 2541 . . . . . . . . . 10  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  E  e.  ( d L E ) )
7574ad3antrrr 741 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  E  e.  ( d L E ) )
7637ad3antrrr 741 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  D  e.  P )
77 acopyeu.1 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  <" A B C "> (cgrA `  G ) <" D E X "> )
781, 18, 2, 11, 22, 25, 19, 33ncolrot2 24656 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  -.  ( C  e.  ( A L B )  \/  A  =  B ) )
791, 2, 17, 11, 19, 22, 25, 36, 14, 4, 77, 18, 78cgrancol 24918 . . . . . . . . . . . . . . 15  |-  ( ph  ->  -.  ( X  e.  ( D L E )  \/  D  =  E ) )
801, 18, 2, 11, 36, 14, 4, 79ncolcom 24654 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  ( X  e.  ( E L D )  \/  E  =  D ) )
8180ad5antr 745 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  ( X  e.  ( E L D )  \/  E  =  D ) )
82 simprlr 778 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  x
( K `  E
) X )
831, 2, 3, 62, 6, 16, 13, 18, 82hlln 24700 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  x  e.  ( X L E ) )
841, 2, 3, 62, 6, 16, 13, 82hlne1 24698 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  x  =/=  E )
851, 2, 18, 13, 6, 16, 76, 62, 81, 83, 84ncolncol 24739 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  ( x  e.  ( E L D )  \/  E  =  D ) )
861, 18, 2, 13, 16, 76, 62, 85ncolcom 24654 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  ( x  e.  ( D L E )  \/  D  =  E ) )
87 pm2.45 403 . . . . . . . . . . 11  |-  ( -.  ( x  e.  ( D L E )  \/  D  =  E )  ->  -.  x  e.  ( D L E ) )
8886, 87syl 17 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  x  e.  ( D L E ) )
8970ad3antrrr 741 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  ( D L E )  =  ( d L E ) )
9089eleq2d 2524 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  (
x  e.  ( D L E )  <->  x  e.  ( d L E ) ) )
9188, 90mtbid 306 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  x  e.  ( d L E ) )
921, 2, 18, 13, 72, 16, 61, 3, 75, 62, 6, 91, 82hphl 24861 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  x
( (hpG `  G
) `  ( d L E ) ) X )
93 acopyeu.3 . . . . . . . . . 10  |-  ( ph  ->  X ( (hpG `  G ) `  ( D L E ) ) F )
9493ad5antr 745 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  X
( (hpG `  G
) `  ( D L E ) ) F )
9570fveq2d 5891 . . . . . . . . . . 11  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( (hpG `  G ) `  ( D L E ) )  =  ( (hpG `  G ) `  (
d L E ) ) )
9695ad3antrrr 741 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  (
(hpG `  G ) `  ( D L E ) )  =  ( (hpG `  G ) `  ( d L E ) ) )
9796breqd 4426 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  ( X ( (hpG `  G ) `  ( D L E ) ) F  <->  X ( (hpG `  G ) `  (
d L E ) ) F ) )
9894, 97mpbid 215 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  X
( (hpG `  G
) `  ( d L E ) ) F )
991, 2, 18, 13, 72, 62, 73, 6, 92, 32, 98hpgtr 24858 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  x
( (hpG `  G
) `  ( d L E ) ) F )
100 acopyeu.2 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  <" A B C "> (cgrA `  G ) <" D E Y "> )
1011, 2, 17, 11, 19, 22, 25, 36, 14, 8, 100, 18, 78cgrancol 24918 . . . . . . . . . . . . . . 15  |-  ( ph  ->  -.  ( Y  e.  ( D L E )  \/  D  =  E ) )
1021, 18, 2, 11, 36, 14, 8, 101ncolcom 24654 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  ( Y  e.  ( E L D )  \/  E  =  D ) )
103102ad5antr 745 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  ( Y  e.  ( E L D )  \/  E  =  D ) )
104 simprrr 780 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  y
( K `  E
) Y )
1051, 2, 3, 7, 10, 16, 13, 18, 104hlln 24700 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  y  e.  ( Y L E ) )
1061, 2, 3, 7, 10, 16, 13, 104hlne1 24698 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  y  =/=  E )
1071, 2, 18, 13, 10, 16, 76, 7, 103, 105, 106ncolncol 24739 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  ( y  e.  ( E L D )  \/  E  =  D ) )
1081, 18, 2, 13, 16, 76, 7, 107ncolcom 24654 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  ( y  e.  ( D L E )  \/  D  =  E ) )
109 pm2.45 403 . . . . . . . . . . 11  |-  ( -.  ( y  e.  ( D L E )  \/  D  =  E )  ->  -.  y  e.  ( D L E ) )
110108, 109syl 17 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  y  e.  ( D L E ) )
11189eleq2d 2524 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  (
y  e.  ( D L E )  <->  y  e.  ( d L E ) ) )
112110, 111mtbid 306 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  -.  y  e.  ( d L E ) )
1131, 2, 18, 13, 72, 16, 61, 3, 75, 7, 10, 112, 104hphl 24861 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  y
( (hpG `  G
) `  ( d L E ) ) Y )
114 acopyeu.4 . . . . . . . . . 10  |-  ( ph  ->  Y ( (hpG `  G ) `  ( D L E ) ) F )
115114ad5antr 745 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  Y
( (hpG `  G
) `  ( D L E ) ) F )
11696breqd 4426 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  ( Y ( (hpG `  G ) `  ( D L E ) ) F  <->  Y ( (hpG `  G ) `  (
d L E ) ) F ) )
117115, 116mpbid 215 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  Y
( (hpG `  G
) `  ( d L E ) ) F )
1181, 2, 18, 13, 72, 7, 73, 10, 113, 32, 117hpgtr 24858 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  y
( (hpG `  G
) `  ( d L E ) ) F )
1191, 17, 2, 18, 3, 13, 21, 24, 27, 29, 16, 32, 35, 44, 48, 61, 62, 7, 63, 64, 99, 118trgcopyeulem 24895 . . . . . 6  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  x  =  y )
120119, 82eqbrtrrd 4438 . . . . 5  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  y
( K `  E
) X )
1211, 2, 3, 7, 6, 16, 13, 120hlcomd 24697 . . . 4  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  X
( K `  E
) y )
1221, 2, 3, 6, 7, 10, 13, 16, 121, 104hltr 24703 . . 3  |-  ( ( ( ( ( (
ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  /\  x  e.  P
)  /\  y  e.  P )  /\  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )  ->  X
( K `  E
) Y )
12377ad2antrr 737 . . . . . 6  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  <" A B C "> (cgrA `  G ) <" D E X "> )
1241, 2, 3, 12, 20, 23, 26, 37, 15, 5, 123, 28, 40cgrahl1 24906 . . . . 5  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  <" A B C "> (cgrA `  G ) <" d E X "> )
1251, 2, 18, 11, 19, 22, 25, 33ncolne1 24718 . . . . . . 7  |-  ( ph  ->  A  =/=  B )
126125ad2antrr 737 . . . . . 6  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  A  =/=  B
)
1271, 2, 3, 12, 20, 23, 26, 28, 15, 5, 17, 126, 47iscgra1 24900 . . . . 5  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( <" A B C "> (cgrA `  G ) <" d E X ">  <->  E. x  e.  P  ( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x
( K `  E
) X ) ) )
128124, 127mpbid 215 . . . 4  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  E. x  e.  P  ( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X ) )
129100ad2antrr 737 . . . . . 6  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  <" A B C "> (cgrA `  G ) <" D E Y "> )
1301, 2, 3, 12, 20, 23, 26, 37, 15, 9, 129, 28, 40cgrahl1 24906 . . . . 5  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  <" A B C "> (cgrA `  G ) <" d E Y "> )
1311, 2, 3, 12, 20, 23, 26, 28, 15, 9, 17, 126, 47iscgra1 24900 . . . . 5  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  ( <" A B C "> (cgrA `  G ) <" d E Y ">  <->  E. y  e.  P  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y
( K `  E
) Y ) ) )
132130, 131mpbid 215 . . . 4  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  E. y  e.  P  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) )
133 reeanv 2969 . . . 4  |-  ( E. x  e.  P  E. y  e.  P  (
( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) )  <->  ( E. x  e.  P  ( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x
( K `  E
) X )  /\  E. y  e.  P  (
<" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )
134128, 132, 133sylanbrc 675 . . 3  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  E. x  e.  P  E. y  e.  P  ( ( <" A B C "> (cgrG `  G ) <" d E x ">  /\  x ( K `  E ) X )  /\  ( <" A B C "> (cgrG `  G ) <" d E y ">  /\  y ( K `  E ) Y ) ) )
135122, 134r19.29vva 2945 . 2  |-  ( ( ( ph  /\  d  e.  P )  /\  (
d ( K `  E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )  ->  X ( K `
 E ) Y )
136125necomd 2690 . . 3  |-  ( ph  ->  B  =/=  A )
1371, 2, 3, 14, 22, 19, 11, 36, 17, 65, 136hlcgrex 24709 . 2  |-  ( ph  ->  E. d  e.  P  ( d ( K `
 E ) D  /\  ( E  .-  d )  =  ( B  .-  A ) ) )
138135, 137r19.29a 2943 1  |-  ( ph  ->  X ( K `  E ) Y )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 374    /\ wa 375    = wceq 1454    e. wcel 1897    =/= wne 2632   E.wrex 2749    \ cdif 3412   class class class wbr 4415   {copab 4473   ran crn 4853   ` cfv 5600  (class class class)co 6314   <"cs3 12974   Basecbs 15169   distcds 15247  TarskiGcstrkg 24526  Itvcitv 24532  LineGclng 24533  cgrGccgrg 24603  hlGchlg 24693  hpGchpg 24847  cgrAccgra 24897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-oadd 7211  df-er 7388  df-map 7499  df-pm 7500  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-card 8398  df-cda 8623  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-2 10695  df-3 10696  df-n0 10898  df-z 10966  df-uz 11188  df-fz 11813  df-fzo 11946  df-hash 12547  df-word 12696  df-concat 12698  df-s1 12699  df-s2 12980  df-s3 12981  df-trkgc 24544  df-trkgb 24545  df-trkgcb 24546  df-trkgld 24548  df-trkg 24549  df-cgrg 24604  df-leg 24676  df-hlg 24694  df-mir 24746  df-rag 24787  df-perpg 24789  df-hpg 24848  df-mid 24864  df-lmi 24865  df-cgra 24898
This theorem is referenced by:  tgasa1  24937
  Copyright terms: Public domain W3C validator