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