Metamath Proof Explorer

Theorem trgcopyeulem

Description: Lemma for trgcopyeu . (Contributed by Thierry Arnoux, 8-Aug-2020)

Ref Expression
Hypotheses trgcopy.p 
|- P = ( Base ` G )
trgcopy.m 
|- .- = ( dist ` G )
trgcopy.i 
|- I = ( Itv ` G )
trgcopy.l 
|- L = ( LineG ` G )
trgcopy.k 
|- K = ( hlG ` G )
trgcopy.g 
|- ( ph -> G e. TarskiG )
trgcopy.a 
|- ( ph -> A e. P )
trgcopy.b 
|- ( ph -> B e. P )
trgcopy.c 
|- ( ph -> C e. P )
trgcopy.d 
|- ( ph -> D e. P )
trgcopy.e 
|- ( ph -> E e. P )
trgcopy.f 
|- ( ph -> F e. P )
trgcopy.1 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
trgcopy.2 
|- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
trgcopy.3 
|- ( ph -> ( A .- B ) = ( D .- E ) )
trgcopyeulem.o 
|- O = { <. 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 ) ) }
trgcopyeulem.x 
|- ( ph -> X e. P )
trgcopyeulem.y 
|- ( ph -> Y e. P )
trgcopyeulem.1 
|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E X "> )
trgcopyeulem.2 
|- ( ph -> <" A B C "> ( cgrG ` G ) <" D E Y "> )
trgcopyeulem.3 
|- ( ph -> X ( ( hpG ` G ) ` ( D L E ) ) F )
trgcopyeulem.4 
|- ( ph -> Y ( ( hpG ` G ) ` ( D L E ) ) F )
Assertion trgcopyeulem 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 trgcopy.p 
 |-  P = ( Base ` G )
2 trgcopy.m 
 |-  .- = ( dist ` G )
3 trgcopy.i 
 |-  I = ( Itv ` G )
4 trgcopy.l 
 |-  L = ( LineG ` G )
5 trgcopy.k 
 |-  K = ( hlG ` G )
6 trgcopy.g 
 |-  ( ph -> G e. TarskiG )
7 trgcopy.a 
 |-  ( ph -> A e. P )
8 trgcopy.b 
 |-  ( ph -> B e. P )
9 trgcopy.c 
 |-  ( ph -> C e. P )
10 trgcopy.d 
 |-  ( ph -> D e. P )
11 trgcopy.e 
 |-  ( ph -> E e. P )
12 trgcopy.f 
 |-  ( ph -> F e. P )
13 trgcopy.1 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
14 trgcopy.2 
 |-  ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
15 trgcopy.3 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
16 trgcopyeulem.o 
 |-  O = { <. 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 ) ) }
17 trgcopyeulem.x 
 |-  ( ph -> X e. P )
18 trgcopyeulem.y 
 |-  ( ph -> Y e. P )
19 trgcopyeulem.1 
 |-  ( ph -> <" A B C "> ( cgrG ` G ) <" D E X "> )
20 trgcopyeulem.2 
 |-  ( ph -> <" A B C "> ( cgrG ` G ) <" D E Y "> )
21 trgcopyeulem.3 
 |-  ( ph -> X ( ( hpG ` G ) ` ( D L E ) ) F )
22 trgcopyeulem.4 
 |-  ( ph -> Y ( ( hpG ` G ) ` ( D L E ) ) F )
23 1 4 3 6 8 9 7 13 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
24 eqid 
 |-  ( ( lInvG ` G ) ` ( D L E ) ) = ( ( lInvG ` G ) ` ( D L E ) )
25 1 3 4 6 10 11 12 14 ncolne1 
 |-  ( ph -> D =/= E )
26 1 3 4 6 10 11 25 tgelrnln 
 |-  ( ph -> ( D L E ) e. ran L )
27 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
28 6 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> G e. TarskiG )
29 26 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( D L E ) e. ran L )
30 simplr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> t e. ( D L E ) )
31 1 4 3 28 29 30 tglnpt 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> t e. P )
32 eqid 
 |-  ( ( pInvG ` G ) ` t ) = ( ( pInvG ` G ) ` t )
33 1 2 3 6 23 24 4 26 18 lmicl 
 |-  ( ph -> ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) e. P )
34 33 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) e. P )
35 17 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> X e. P )
36 10 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> D e. P )
37 11 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> E e. P )
38 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
39 25 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> D =/= E )
40 39 necomd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> E =/= D )
41 1 3 4 28 37 36 31 40 30 lncom 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> t e. ( E L D ) )
42 41 orcd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( t e. ( E L D ) \/ E = D ) )
43 1 4 3 28 37 36 31 42 colrot1 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( E e. ( D L t ) \/ D = t ) )
44 1 2 3 38 6 7 8 9 10 11 17 19 cgr3simp3 
 |-  ( ph -> ( C .- A ) = ( X .- D ) )
45 1 2 3 6 9 7 17 10 44 tgcgrcomlr 
 |-  ( ph -> ( A .- C ) = ( D .- X ) )
46 1 2 3 38 6 7 8 9 10 11 18 20 cgr3simp3 
 |-  ( ph -> ( C .- A ) = ( Y .- D ) )
47 1 2 3 6 9 7 18 10 46 tgcgrcomlr 
 |-  ( ph -> ( A .- C ) = ( D .- Y ) )
48 45 47 eqtr3d 
 |-  ( ph -> ( D .- X ) = ( D .- Y ) )
49 1 2 3 6 23 24 4 26 10 18 lmiiso 
 |-  ( ph -> ( ( ( ( lInvG ` G ) ` ( D L E ) ) ` D ) .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = ( D .- Y ) )
50 1 3 4 6 10 11 25 tglinerflx1 
 |-  ( ph -> D e. ( D L E ) )
51 1 2 3 6 23 24 4 26 10 50 lmicinv 
 |-  ( ph -> ( ( ( lInvG ` G ) ` ( D L E ) ) ` D ) = D )
52 51 oveq1d 
 |-  ( ph -> ( ( ( ( lInvG ` G ) ` ( D L E ) ) ` D ) .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = ( D .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
53 48 49 52 3eqtr2d 
 |-  ( ph -> ( D .- X ) = ( D .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
54 53 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( D .- X ) = ( D .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
55 1 2 3 38 6 7 8 9 10 11 17 19 cgr3simp2 
 |-  ( ph -> ( B .- C ) = ( E .- X ) )
56 1 2 3 38 6 7 8 9 10 11 18 20 cgr3simp2 
 |-  ( ph -> ( B .- C ) = ( E .- Y ) )
57 55 56 eqtr3d 
 |-  ( ph -> ( E .- X ) = ( E .- Y ) )
58 1 2 3 6 23 24 4 26 11 18 lmiiso 
 |-  ( ph -> ( ( ( ( lInvG ` G ) ` ( D L E ) ) ` E ) .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = ( E .- Y ) )
59 1 3 4 6 10 11 25 tglinerflx2 
 |-  ( ph -> E e. ( D L E ) )
60 1 2 3 6 23 24 4 26 11 59 lmicinv 
 |-  ( ph -> ( ( ( lInvG ` G ) ` ( D L E ) ) ` E ) = E )
61 60 oveq1d 
 |-  ( ph -> ( ( ( ( lInvG ` G ) ` ( D L E ) ) ` E ) .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = ( E .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
62 57 58 61 3eqtr2d 
 |-  ( ph -> ( E .- X ) = ( E .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
63 62 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( E .- X ) = ( E .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
64 1 4 3 28 36 37 31 38 35 34 2 39 43 54 63 lncgr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( t .- X ) = ( t .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
65 simpr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
66 1 2 3 4 27 28 31 32 34 35 64 65 ismir 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> X = ( ( ( pInvG ` G ) ` t ) ` ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
67 66 eqcomd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( ( ( pInvG ` G ) ` t ) ` ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = X )
68 1 2 3 4 27 28 31 32 34 67 mircom 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( ( ( pInvG ` G ) ` t ) ` X ) = ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) )
69 68 eqcomd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) = ( ( ( pInvG ` G ) ` t ) ` X ) )
70 23 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> G TarskiGDim>= 2 )
71 1 2 3 28 70 35 34 27 31 ismidb 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) = ( ( ( pInvG ` G ) ` t ) ` X ) <-> ( X ( midG ` G ) ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = t ) )
72 69 71 mpbid 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( X ( midG ` G ) ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = t )
73 72 30 eqeltrd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( X ( midG ` G ) ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) e. ( D L E ) )
74 1 3 4 6 26 17 16 12 21 hpgcom 
 |-  ( ph -> F ( ( hpG ` G ) ` ( D L E ) ) X )
75 1 3 4 6 26 18 16 12 22 17 74 hpgtr 
 |-  ( ph -> Y ( ( hpG ` G ) ` ( D L E ) ) X )
76 1 3 4 16 6 26 18 12 22 hpgne1 
 |-  ( ph -> -. Y e. ( D L E ) )
77 1 2 3 4 6 23 26 16 24 18 76 lmiopp 
 |-  ( ph -> Y O ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) )
78 1 3 4 16 6 26 18 17 33 77 lnopp2hpgb 
 |-  ( ph -> ( X O ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) <-> Y ( ( hpG ` G ) ` ( D L E ) ) X ) )
79 75 78 mpbird 
 |-  ( ph -> X O ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) )
80 1 2 3 16 17 33 islnopp 
 |-  ( ph -> ( X O ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) <-> ( ( -. X e. ( D L E ) /\ -. ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) e. ( D L E ) ) /\ E. t e. ( D L E ) t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) ) )
81 79 80 mpbid 
 |-  ( ph -> ( ( -. X e. ( D L E ) /\ -. ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) e. ( D L E ) ) /\ E. t e. ( D L E ) t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) )
82 81 simprd 
 |-  ( ph -> E. t e. ( D L E ) t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
83 73 82 r19.29a 
 |-  ( ph -> ( X ( midG ` G ) ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) e. ( D L E ) )
84 28 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> G e. TarskiG )
85 29 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> ( D L E ) e. ran L )
86 1 2 3 16 4 26 6 17 33 79 oppne3 
 |-  ( ph -> X =/= ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) )
87 1 3 4 6 17 33 86 tgelrnln 
 |-  ( ph -> ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) e. ran L )
88 87 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) e. ran L )
89 88 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) e. ran L )
90 86 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> X =/= ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) )
91 1 3 4 28 35 34 31 90 65 btwnlng1 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> t e. ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
92 30 91 elind 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> t e. ( ( D L E ) i^i ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) )
93 92 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> t e. ( ( D L E ) i^i ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) )
94 59 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> E e. ( D L E ) )
95 1 3 4 6 17 33 86 tglinerflx1 
 |-  ( ph -> X e. ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
96 95 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> X e. ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
97 simpr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> E =/= t )
98 81 simplld 
 |-  ( ph -> -. X e. ( D L E ) )
99 98 ad2antrr 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> -. X e. ( D L E ) )
100 nelne2 
 |-  ( ( t e. ( D L E ) /\ -. X e. ( D L E ) ) -> t =/= X )
101 30 99 100 syl2anc 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> t =/= X )
102 101 necomd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> X =/= t )
103 102 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> X =/= t )
104 69 oveq2d 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( E .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = ( E .- ( ( ( pInvG ` G ) ` t ) ` X ) ) )
105 63 104 eqtrd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( E .- X ) = ( E .- ( ( ( pInvG ` G ) ` t ) ` X ) ) )
106 105 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> ( E .- X ) = ( E .- ( ( ( pInvG ` G ) ` t ) ` X ) ) )
107 37 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> E e. P )
108 31 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> t e. P )
109 35 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> X e. P )
110 1 2 3 4 27 84 107 108 109 israg 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> ( <" E t X "> e. ( raG ` G ) <-> ( E .- X ) = ( E .- ( ( ( pInvG ` G ) ` t ) ` X ) ) ) )
111 106 110 mpbird 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> <" E t X "> e. ( raG ` G ) )
112 1 2 3 4 84 85 89 93 94 96 97 103 111 ragperp 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ E =/= t ) -> ( D L E ) ( perpG ` G ) ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
113 28 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> G e. TarskiG )
114 29 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> ( D L E ) e. ran L )
115 88 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) e. ran L )
116 92 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> t e. ( ( D L E ) i^i ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) )
117 50 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> D e. ( D L E ) )
118 95 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> X e. ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
119 simpr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> D =/= t )
120 102 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> X =/= t )
121 69 oveq2d 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( D .- ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) = ( D .- ( ( ( pInvG ` G ) ` t ) ` X ) ) )
122 54 121 eqtrd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( D .- X ) = ( D .- ( ( ( pInvG ` G ) ` t ) ` X ) ) )
123 122 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> ( D .- X ) = ( D .- ( ( ( pInvG ` G ) ` t ) ` X ) ) )
124 36 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> D e. P )
125 31 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> t e. P )
126 35 adantr 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> X e. P )
127 1 2 3 4 27 113 124 125 126 israg 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> ( <" D t X "> e. ( raG ` G ) <-> ( D .- X ) = ( D .- ( ( ( pInvG ` G ) ` t ) ` X ) ) ) )
128 123 127 mpbird 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> <" D t X "> e. ( raG ` G ) )
129 1 2 3 4 113 114 115 116 117 118 119 120 128 ragperp 
 |-  ( ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) /\ D =/= t ) -> ( D L E ) ( perpG ` G ) ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
130 neneor 
 |-  ( E =/= D -> ( E =/= t \/ D =/= t ) )
131 40 130 syl 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( E =/= t \/ D =/= t ) )
132 112 129 131 mpjaodan 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( D L E ) ( perpG ` G ) ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
133 132 orcd 
 |-  ( ( ( ph /\ t e. ( D L E ) ) /\ t e. ( X I ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) -> ( ( D L E ) ( perpG ` G ) ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) \/ X = ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
134 133 82 r19.29a 
 |-  ( ph -> ( ( D L E ) ( perpG ` G ) ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) \/ X = ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) )
135 1 2 3 6 23 24 4 26 17 33 islmib 
 |-  ( ph -> ( ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) = ( ( ( lInvG ` G ) ` ( D L E ) ) ` X ) <-> ( ( X ( midG ` G ) ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) e. ( D L E ) /\ ( ( D L E ) ( perpG ` G ) ( X L ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) \/ X = ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) ) ) ) )
136 83 134 135 mpbir2and 
 |-  ( ph -> ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) = ( ( ( lInvG ` G ) ` ( D L E ) ) ` X ) )
137 136 eqcomd 
 |-  ( ph -> ( ( ( lInvG ` G ) ` ( D L E ) ) ` X ) = ( ( ( lInvG ` G ) ` ( D L E ) ) ` Y ) )
138 1 2 3 6 23 24 4 26 17 18 137 lmieq 
 |-  ( ph -> X = Y )