Metamath Proof Explorer

Theorem acopyeu

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)

Ref Expression
Hypotheses 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 acopyeu 
|- ( ph -> X ( K ` E ) Y )

Proof

Step Hyp Ref Expression
1 dfcgra2.p 
 |-  P = ( Base ` G )
2 dfcgra2.i 
 |-  I = ( Itv ` G )
3 dfcgra2.m 
 |-  .- = ( dist ` G )
4 dfcgra2.g 
 |-  ( ph -> G e. TarskiG )
5 dfcgra2.a 
 |-  ( ph -> A e. P )
6 dfcgra2.b 
 |-  ( ph -> B e. P )
7 dfcgra2.c 
 |-  ( ph -> C e. P )
8 dfcgra2.d 
 |-  ( ph -> D e. P )
9 dfcgra2.e 
 |-  ( ph -> E e. P )
10 dfcgra2.f 
 |-  ( ph -> F e. P )
11 acopy.l 
 |-  L = ( LineG ` G )
12 acopy.1 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
13 acopy.2 
 |-  ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
14 acopyeu.x 
 |-  ( ph -> X e. P )
15 acopyeu.y 
 |-  ( ph -> Y e. P )
16 acopyeu.k 
 |-  K = ( hlG ` G )
17 acopyeu.1 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E X "> )
18 acopyeu.2 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E Y "> )
19 acopyeu.3 
 |-  ( ph -> X ( ( hpG ` G ) ` ( D L E ) ) F )
20 acopyeu.4 
 |-  ( ph -> Y ( ( hpG ` G ) ` ( D L E ) ) F )
21 14 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> X e. P )
22 21 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
23 simplr 
 |-  ( ( ( ( ( ( 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 )
24 15 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> Y e. P )
25 24 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
26 4 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> G e. TarskiG )
27 26 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
28 9 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> E e. P )
29 28 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
30 5 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> A e. P )
31 30 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
32 6 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> B e. P )
33 32 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
34 7 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> C e. P )
35 34 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
36 simplr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> d e. P )
37 36 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
38 10 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> F e. P )
39 38 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
40 12 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> -. ( A e. ( B L C ) \/ B = C ) )
41 40 ad3antrrr 
 |-  ( ( ( ( ( ( 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 ) )
42 8 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> D e. P )
43 13 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> -. ( D e. ( E L F ) \/ E = F ) )
44 simprl 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> d ( K ` E ) D )
45 1 2 16 36 42 28 26 11 44 hlln 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> d e. ( D L E ) )
46 1 2 16 36 42 28 26 44 hlne1 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> d =/= E )
47 1 2 11 26 42 28 38 36 43 45 46 ncolncol 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> -. ( d e. ( E L F ) \/ E = F ) )
48 47 ad3antrrr 
 |-  ( ( ( ( ( ( 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 ) )
49 simprr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( E .- d ) = ( B .- A ) )
50 1 3 2 26 28 36 32 30 49 tgcgrcomlr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( d .- E ) = ( A .- B ) )
51 50 eqcomd 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( A .- B ) = ( d .- E ) )
52 51 ad3antrrr 
 |-  ( ( ( ( ( ( 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 ) )
53 simpl 
 |-  ( ( u = a /\ v = b ) -> u = a )
54 53 eleq1d 
 |-  ( ( u = a /\ v = b ) -> ( u e. ( P \ ( d L E ) ) <-> a e. ( P \ ( d L E ) ) ) )
55 simpr 
 |-  ( ( u = a /\ v = b ) -> v = b )
56 55 eleq1d 
 |-  ( ( u = a /\ v = b ) -> ( v e. ( P \ ( d L E ) ) <-> b e. ( P \ ( d L E ) ) ) )
57 54 56 anbi12d 
 |-  ( ( 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 ) ) ) ) )
58 simpr 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> w = t )
59 simpll 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> u = a )
60 simplr 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> v = b )
61 59 60 oveq12d 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> ( u I v ) = ( a I b ) )
62 58 61 eleq12d 
 |-  ( ( ( u = a /\ v = b ) /\ w = t ) -> ( w e. ( u I v ) <-> t e. ( a I b ) ) )
63 62 cbvrexdva 
 |-  ( ( 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 ) ) )
64 57 63 anbi12d 
 |-  ( ( 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 ) ) ) )
65 64 cbvopabv 
 |-  { <. 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 ) ) }
66 simpllr 
 |-  ( ( ( ( ( ( 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 )
67 simprll 
 |-  ( ( ( ( ( ( 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 "> )
68 simprrl 
 |-  ( ( ( ( ( ( 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 "> )
69 1 2 11 26 36 28 46 tgelrnln 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( d L E ) e. ran L )
70 69 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
71 1 2 11 26 36 28 46 tglinerflx2 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> E e. ( d L E ) )
72 71 ad3antrrr 
 |-  ( ( ( ( ( ( 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 ) )
73 42 ad3antrrr 
 |-  ( ( ( ( ( ( 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 )
74 1 11 2 4 6 7 5 12 ncolrot2 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
75 1 2 3 4 5 6 7 8 9 14 17 11 74 cgrancol 
 |-  ( ph -> -. ( X e. ( D L E ) \/ D = E ) )
76 1 11 2 4 8 9 14 75 ncolcom 
 |-  ( ph -> -. ( X e. ( E L D ) \/ E = D ) )
77 76 ad5antr 
 |-  ( ( ( ( ( ( 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 ) )
78 simprlr 
 |-  ( ( ( ( ( ( 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 )
79 1 2 16 66 22 29 27 11 78 hlln 
 |-  ( ( ( ( ( ( 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 ) )
80 1 2 16 66 22 29 27 78 hlne1 
 |-  ( ( ( ( ( ( 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 )
81 1 2 11 27 22 29 73 66 77 79 80 ncolncol 
 |-  ( ( ( ( ( ( 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 1 11 2 27 29 73 66 81 ncolcom 
 |-  ( ( ( ( ( ( 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 ) )
83 pm2.45 
 |-  ( -. ( x e. ( D L E ) \/ D = E ) -> -. x e. ( D L E ) )
84 82 83 syl 
 |-  ( ( ( ( ( ( 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 ) )
85 1 2 11 4 8 9 10 13 ncolne1 
 |-  ( ph -> D =/= E )
86 1 2 11 4 8 9 85 tgelrnln 
 |-  ( ph -> ( D L E ) e. ran L )
87 86 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( D L E ) e. ran L )
88 1 2 11 4 8 9 85 tglinerflx2 
 |-  ( ph -> E e. ( D L E ) )
89 88 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> E e. ( D L E ) )
90 1 2 11 26 36 28 46 46 87 45 89 tglinethru 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( D L E ) = ( d L E ) )
91 90 ad3antrrr 
 |-  ( ( ( ( ( ( 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 ) )
92 84 91 neleqtrd 
 |-  ( ( ( ( ( ( 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 ) )
93 1 2 11 27 70 29 65 16 72 66 22 92 78 hphl 
 |-  ( ( ( ( ( ( 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 )
94 90 fveq2d 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> ( ( hpG ` G ) ` ( D L E ) ) = ( ( hpG ` G ) ` ( d L E ) ) )
95 94 ad3antrrr 
 |-  ( ( ( ( ( ( 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 ) ) )
96 19 ad5antr 
 |-  ( ( ( ( ( ( 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 )
97 95 96 breqdi 
 |-  ( ( ( ( ( ( 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 )
98 1 2 11 27 70 66 65 22 93 39 97 hpgtr 
 |-  ( ( ( ( ( ( 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 )
99 1 2 3 4 5 6 7 8 9 15 18 11 74 cgrancol 
 |-  ( ph -> -. ( Y e. ( D L E ) \/ D = E ) )
100 1 11 2 4 8 9 15 99 ncolcom 
 |-  ( ph -> -. ( Y e. ( E L D ) \/ E = D ) )
101 100 ad5antr 
 |-  ( ( ( ( ( ( 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 ) )
102 simprrr 
 |-  ( ( ( ( ( ( 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 )
103 1 2 16 23 25 29 27 11 102 hlln 
 |-  ( ( ( ( ( ( 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 ) )
104 1 2 16 23 25 29 27 102 hlne1 
 |-  ( ( ( ( ( ( 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 )
105 1 2 11 27 25 29 73 23 101 103 104 ncolncol 
 |-  ( ( ( ( ( ( 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 ) )
106 1 11 2 27 29 73 23 105 ncolcom 
 |-  ( ( ( ( ( ( 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 ) )
107 pm2.45 
 |-  ( -. ( y e. ( D L E ) \/ D = E ) -> -. y e. ( D L E ) )
108 106 107 syl 
 |-  ( ( ( ( ( ( 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 ) )
109 108 91 neleqtrd 
 |-  ( ( ( ( ( ( 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 ) )
110 1 2 11 27 70 29 65 16 72 23 25 109 102 hphl 
 |-  ( ( ( ( ( ( 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 )
111 20 ad5antr 
 |-  ( ( ( ( ( ( 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 )
112 95 111 breqdi 
 |-  ( ( ( ( ( ( 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 )
113 1 2 11 27 70 23 65 25 110 39 112 hpgtr 
 |-  ( ( ( ( ( ( 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 )
114 1 3 2 11 16 27 31 33 35 37 29 39 41 48 52 65 66 23 67 68 98 113 trgcopyeulem 
 |-  ( ( ( ( ( ( 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 )
115 114 78 eqbrtrrd 
 |-  ( ( ( ( ( ( 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 )
116 1 2 16 23 22 29 27 115 hlcomd 
 |-  ( ( ( ( ( ( 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 )
117 1 2 16 22 23 25 27 29 116 102 hltr 
 |-  ( ( ( ( ( ( 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 )
118 17 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E X "> )
119 1 2 16 26 30 32 34 42 28 21 118 36 44 cgrahl1 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> <" A B C "> ( cgrA ` G ) <" d E X "> )
120 1 2 11 4 5 6 7 12 ncolne1 
 |-  ( ph -> A =/= B )
121 120 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> A =/= B )
122 1 2 16 26 30 32 34 36 28 21 3 121 51 iscgra1 
 |-  ( ( ( 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 ) ) )
123 119 122 mpbid 
 |-  ( ( ( 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 ) )
124 18 ad2antrr 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E Y "> )
125 1 2 16 26 30 32 34 42 28 24 124 36 44 cgrahl1 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> <" A B C "> ( cgrA ` G ) <" d E Y "> )
126 1 2 16 26 30 32 34 36 28 24 3 121 51 iscgra1 
 |-  ( ( ( 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 ) ) )
127 125 126 mpbid 
 |-  ( ( ( 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 ) )
128 reeanv 
 |-  ( 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 ) ) )
129 123 127 128 sylanbrc 
 |-  ( ( ( 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 ) ) )
130 117 129 r19.29vva 
 |-  ( ( ( ph /\ d e. P ) /\ ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) ) -> X ( K ` E ) Y )
131 120 necomd 
 |-  ( ph -> B =/= A )
132 1 2 16 9 6 5 4 8 3 85 131 hlcgrex 
 |-  ( ph -> E. d e. P ( d ( K ` E ) D /\ ( E .- d ) = ( B .- A ) ) )
133 130 132 r19.29a 
 |-  ( ph -> X ( K ` E ) Y )