Metamath Proof Explorer


Theorem lmiisolem

Description: Lemma for lmiiso . (Contributed by Thierry Arnoux, 14-Dec-2019)

Ref Expression
Hypotheses ismid.p P = Base G
ismid.d - ˙ = dist G
ismid.i I = Itv G
ismid.g φ G 𝒢 Tarski
ismid.1 φ G Dim 𝒢 2
lmif.m M = lInv 𝒢 G D
lmif.l L = Line 𝒢 G
lmif.d φ D ran L
lmiiso.1 φ A P
lmiiso.2 φ B P
lmiisolem.s S = pInv 𝒢 G Z
lmiisolem.z Z = A mid 𝒢 G M A mid 𝒢 G B mid 𝒢 G M B
Assertion lmiisolem φ M A - ˙ M B = A - ˙ B

Proof

Step Hyp Ref Expression
1 ismid.p P = Base G
2 ismid.d - ˙ = dist G
3 ismid.i I = Itv G
4 ismid.g φ G 𝒢 Tarski
5 ismid.1 φ G Dim 𝒢 2
6 lmif.m M = lInv 𝒢 G D
7 lmif.l L = Line 𝒢 G
8 lmif.d φ D ran L
9 lmiiso.1 φ A P
10 lmiiso.2 φ B P
11 lmiisolem.s S = pInv 𝒢 G Z
12 lmiisolem.z Z = A mid 𝒢 G M A mid 𝒢 G B mid 𝒢 G M B
13 4 adantr φ S A = Z G 𝒢 Tarski
14 1 2 3 4 5 6 7 8 9 lmicl φ M A P
15 1 2 3 4 5 9 14 midcl φ A mid 𝒢 G M A P
16 1 2 3 4 5 6 7 8 10 lmicl φ M B P
17 1 2 3 4 5 10 16 midcl φ B mid 𝒢 G M B P
18 1 2 3 4 5 15 17 midcl φ A mid 𝒢 G M A mid 𝒢 G B mid 𝒢 G M B P
19 12 18 eqeltrid φ Z P
20 19 adantr φ S A = Z Z P
21 eqid pInv 𝒢 G = pInv 𝒢 G
22 1 2 3 7 21 4 19 11 9 mircl φ S A P
23 22 adantr φ S A = Z S A P
24 9 adantr φ S A = Z A P
25 1 2 3 7 21 13 20 11 24 mircgr φ S A = Z Z - ˙ S A = Z - ˙ A
26 simpr φ S A = Z S A = Z
27 26 eqcomd φ S A = Z Z = S A
28 1 2 3 13 20 23 20 24 25 27 tgcgreq φ S A = Z Z = A
29 simpr φ A mid 𝒢 G M A = B mid 𝒢 G M B A mid 𝒢 G M A = B mid 𝒢 G M B
30 29 oveq2d φ A mid 𝒢 G M A = B mid 𝒢 G M B A mid 𝒢 G M A mid 𝒢 G A mid 𝒢 G M A = A mid 𝒢 G M A mid 𝒢 G B mid 𝒢 G M B
31 12 30 eqtr4id φ A mid 𝒢 G M A = B mid 𝒢 G M B Z = A mid 𝒢 G M A mid 𝒢 G A mid 𝒢 G M A
32 4 adantr φ A mid 𝒢 G M A = B mid 𝒢 G M B G 𝒢 Tarski
33 5 adantr φ A mid 𝒢 G M A = B mid 𝒢 G M B G Dim 𝒢 2
34 15 adantr φ A mid 𝒢 G M A = B mid 𝒢 G M B A mid 𝒢 G M A P
35 1 2 3 32 33 34 34 midid φ A mid 𝒢 G M A = B mid 𝒢 G M B A mid 𝒢 G M A mid 𝒢 G A mid 𝒢 G M A = A mid 𝒢 G M A
36 31 35 eqtrd φ A mid 𝒢 G M A = B mid 𝒢 G M B Z = A mid 𝒢 G M A
37 eqidd φ M A = M A
38 1 2 3 4 5 6 7 8 9 14 islmib φ M A = M A A mid 𝒢 G M A D D 𝒢 G A L M A A = M A
39 37 38 mpbid φ A mid 𝒢 G M A D D 𝒢 G A L M A A = M A
40 39 simpld φ A mid 𝒢 G M A D
41 40 adantr φ A mid 𝒢 G M A = B mid 𝒢 G M B A mid 𝒢 G M A D
42 36 41 eqeltrd φ A mid 𝒢 G M A = B mid 𝒢 G M B Z D
43 4 adantr φ A mid 𝒢 G M A B mid 𝒢 G M B G 𝒢 Tarski
44 15 adantr φ A mid 𝒢 G M A B mid 𝒢 G M B A mid 𝒢 G M A P
45 17 adantr φ A mid 𝒢 G M A B mid 𝒢 G M B B mid 𝒢 G M B P
46 19 adantr φ A mid 𝒢 G M A B mid 𝒢 G M B Z P
47 simpr φ A mid 𝒢 G M A B mid 𝒢 G M B A mid 𝒢 G M A B mid 𝒢 G M B
48 1 2 3 4 5 15 17 midbtwn φ A mid 𝒢 G M A mid 𝒢 G B mid 𝒢 G M B A mid 𝒢 G M A I B mid 𝒢 G M B
49 12 48 eqeltrid φ Z A mid 𝒢 G M A I B mid 𝒢 G M B
50 49 adantr φ A mid 𝒢 G M A B mid 𝒢 G M B Z A mid 𝒢 G M A I B mid 𝒢 G M B
51 1 3 7 43 44 45 46 47 50 btwnlng1 φ A mid 𝒢 G M A B mid 𝒢 G M B Z A mid 𝒢 G M A L B mid 𝒢 G M B
52 8 adantr φ A mid 𝒢 G M A B mid 𝒢 G M B D ran L
53 40 adantr φ A mid 𝒢 G M A B mid 𝒢 G M B A mid 𝒢 G M A D
54 eqidd φ M B = M B
55 1 2 3 4 5 6 7 8 10 16 islmib φ M B = M B B mid 𝒢 G M B D D 𝒢 G B L M B B = M B
56 54 55 mpbid φ B mid 𝒢 G M B D D 𝒢 G B L M B B = M B
57 56 simpld φ B mid 𝒢 G M B D
58 57 adantr φ A mid 𝒢 G M A B mid 𝒢 G M B B mid 𝒢 G M B D
59 1 3 7 43 44 45 47 47 52 53 58 tglinethru φ A mid 𝒢 G M A B mid 𝒢 G M B D = A mid 𝒢 G M A L B mid 𝒢 G M B
60 51 59 eleqtrrd φ A mid 𝒢 G M A B mid 𝒢 G M B Z D
61 42 60 pm2.61dane φ Z D
62 61 adantr φ S A = Z Z D
63 28 62 eqeltrrd φ S A = Z A D
64 1 2 3 4 5 6 7 8 9 lmiinv φ M A = A A D
65 64 biimpar φ A D M A = A
66 63 65 syldan φ S A = Z M A = A
67 66 28 eqtr4d φ S A = Z M A = Z
68 67 oveq1d φ S A = Z M A - ˙ M B = Z - ˙ M B
69 eqidd φ B = M B Z = Z
70 4 adantr φ B = M B G 𝒢 Tarski
71 10 adantr φ B = M B B P
72 17 adantr φ B = M B B mid 𝒢 G M B P
73 1 2 3 4 5 10 16 midbtwn φ B mid 𝒢 G M B B I M B
74 73 adantr φ B = M B B mid 𝒢 G M B B I M B
75 simpr φ B = M B B = M B
76 75 oveq2d φ B = M B B I B = B I M B
77 74 76 eleqtrrd φ B = M B B mid 𝒢 G M B B I B
78 1 2 3 70 71 72 77 axtgbtwnid φ B = M B B = B mid 𝒢 G M B
79 eqidd φ B = M B B = B
80 69 78 79 s3eqd φ B = M B ⟨“ ZBB ”⟩ = ⟨“ ZB mid 𝒢 G M B B ”⟩
81 1 2 3 7 21 4 19 10 10 ragtrivb φ ⟨“ ZBB ”⟩ 𝒢 G
82 81 adantr φ B = M B ⟨“ ZBB ”⟩ 𝒢 G
83 80 82 eqeltrrd φ B = M B ⟨“ ZB mid 𝒢 G M B B ”⟩ 𝒢 G
84 4 adantr φ B M B G 𝒢 Tarski
85 61 adantr φ B M B Z D
86 57 adantr φ B M B B mid 𝒢 G M B D
87 10 adantr φ B M B B P
88 df-ne B M B ¬ B = M B
89 56 simprd φ D 𝒢 G B L M B B = M B
90 89 orcomd φ B = M B D 𝒢 G B L M B
91 90 orcanai φ ¬ B = M B D 𝒢 G B L M B
92 88 91 sylan2b φ B M B D 𝒢 G B L M B
93 16 adantr φ B M B M B P
94 simpr φ B M B B M B
95 17 adantr φ B M B B mid 𝒢 G M B P
96 4 adantr φ B mid 𝒢 G M B = B G 𝒢 Tarski
97 10 adantr φ B mid 𝒢 G M B = B B P
98 16 adantr φ B mid 𝒢 G M B = B M B P
99 5 adantr φ B mid 𝒢 G M B = B G Dim 𝒢 2
100 simpr φ B mid 𝒢 G M B = B B mid 𝒢 G M B = B
101 1 2 3 96 99 97 98 100 midcgr φ B mid 𝒢 G M B = B B - ˙ B = B - ˙ M B
102 101 eqcomd φ B mid 𝒢 G M B = B B - ˙ M B = B - ˙ B
103 1 2 3 96 97 98 97 102 axtgcgrid φ B mid 𝒢 G M B = B B = M B
104 103 ex φ B mid 𝒢 G M B = B B = M B
105 104 necon3d φ B M B B mid 𝒢 G M B B
106 105 imp φ B M B B mid 𝒢 G M B B
107 73 adantr φ B M B B mid 𝒢 G M B B I M B
108 1 3 7 84 87 93 95 94 107 btwnlng1 φ B M B B mid 𝒢 G M B B L M B
109 1 3 7 84 87 93 94 95 106 108 tglineelsb2 φ B M B B L M B = B L B mid 𝒢 G M B
110 1 3 7 84 95 87 106 tglinecom φ B M B B mid 𝒢 G M B L B = B L B mid 𝒢 G M B
111 109 110 eqtr4d φ B M B B L M B = B mid 𝒢 G M B L B
112 92 111 breqtrd φ B M B D 𝒢 G B mid 𝒢 G M B L B
113 1 2 3 7 84 85 86 87 112 perpdrag φ B M B ⟨“ ZB mid 𝒢 G M B B ”⟩ 𝒢 G
114 83 113 pm2.61dane φ ⟨“ ZB mid 𝒢 G M B B ”⟩ 𝒢 G
115 1 2 3 7 21 4 19 17 10 israg φ ⟨“ ZB mid 𝒢 G M B B ”⟩ 𝒢 G Z - ˙ B = Z - ˙ pInv 𝒢 G B mid 𝒢 G M B B
116 114 115 mpbid φ Z - ˙ B = Z - ˙ pInv 𝒢 G B mid 𝒢 G M B B
117 eqidd φ B mid 𝒢 G M B = B mid 𝒢 G M B
118 1 2 3 4 5 10 16 21 17 ismidb φ M B = pInv 𝒢 G B mid 𝒢 G M B B B mid 𝒢 G M B = B mid 𝒢 G M B
119 117 118 mpbird φ M B = pInv 𝒢 G B mid 𝒢 G M B B
120 119 oveq2d φ Z - ˙ M B = Z - ˙ pInv 𝒢 G B mid 𝒢 G M B B
121 116 120 eqtr4d φ Z - ˙ B = Z - ˙ M B
122 121 adantr φ S A = Z Z - ˙ B = Z - ˙ M B
123 28 oveq1d φ S A = Z Z - ˙ B = A - ˙ B
124 68 122 123 3eqtr2d φ S A = Z M A - ˙ M B = A - ˙ B
125 4 adantr φ S A Z G 𝒢 Tarski
126 22 adantr φ S A Z S A P
127 19 adantr φ S A Z Z P
128 9 adantr φ S A Z A P
129 1 2 3 7 21 4 19 11 14 mircl φ S M A P
130 129 adantr φ S A Z S M A P
131 14 adantr φ S A Z M A P
132 10 adantr φ S A Z B P
133 16 adantr φ S A Z M B P
134 simpr φ S A Z S A Z
135 1 2 3 7 21 125 127 11 128 mirbtwn φ S A Z Z S A I A
136 1 2 3 7 21 125 127 11 131 mirbtwn φ S A Z Z S M A I M A
137 eqidd φ A = M A Z = Z
138 4 adantr φ A = M A G 𝒢 Tarski
139 9 adantr φ A = M A A P
140 15 adantr φ A = M A A mid 𝒢 G M A P
141 1 2 3 4 5 9 14 midbtwn φ A mid 𝒢 G M A A I M A
142 141 adantr φ A = M A A mid 𝒢 G M A A I M A
143 simpr φ A = M A A = M A
144 143 oveq2d φ A = M A A I A = A I M A
145 142 144 eleqtrrd φ A = M A A mid 𝒢 G M A A I A
146 1 2 3 138 139 140 145 axtgbtwnid φ A = M A A = A mid 𝒢 G M A
147 eqidd φ A = M A A = A
148 137 146 147 s3eqd φ A = M A ⟨“ ZAA ”⟩ = ⟨“ ZA mid 𝒢 G M A A ”⟩
149 1 2 3 7 21 4 19 9 9 ragtrivb φ ⟨“ ZAA ”⟩ 𝒢 G
150 149 adantr φ A = M A ⟨“ ZAA ”⟩ 𝒢 G
151 148 150 eqeltrrd φ A = M A ⟨“ ZA mid 𝒢 G M A A ”⟩ 𝒢 G
152 4 adantr φ A M A G 𝒢 Tarski
153 61 adantr φ A M A Z D
154 40 adantr φ A M A A mid 𝒢 G M A D
155 9 adantr φ A M A A P
156 df-ne A M A ¬ A = M A
157 39 simprd φ D 𝒢 G A L M A A = M A
158 157 orcomd φ A = M A D 𝒢 G A L M A
159 158 orcanai φ ¬ A = M A D 𝒢 G A L M A
160 156 159 sylan2b φ A M A D 𝒢 G A L M A
161 14 adantr φ A M A M A P
162 simpr φ A M A A M A
163 15 adantr φ A M A A mid 𝒢 G M A P
164 4 adantr φ A mid 𝒢 G M A = A G 𝒢 Tarski
165 9 adantr φ A mid 𝒢 G M A = A A P
166 14 adantr φ A mid 𝒢 G M A = A M A P
167 5 adantr φ A mid 𝒢 G M A = A G Dim 𝒢 2
168 simpr φ A mid 𝒢 G M A = A A mid 𝒢 G M A = A
169 1 2 3 164 167 165 166 168 midcgr φ A mid 𝒢 G M A = A A - ˙ A = A - ˙ M A
170 169 eqcomd φ A mid 𝒢 G M A = A A - ˙ M A = A - ˙ A
171 1 2 3 164 165 166 165 170 axtgcgrid φ A mid 𝒢 G M A = A A = M A
172 171 ex φ A mid 𝒢 G M A = A A = M A
173 172 necon3d φ A M A A mid 𝒢 G M A A
174 173 imp φ A M A A mid 𝒢 G M A A
175 141 adantr φ A M A A mid 𝒢 G M A A I M A
176 1 3 7 152 155 161 163 162 175 btwnlng1 φ A M A A mid 𝒢 G M A A L M A
177 1 3 7 152 155 161 162 163 174 176 tglineelsb2 φ A M A A L M A = A L A mid 𝒢 G M A
178 1 3 7 152 163 155 174 tglinecom φ A M A A mid 𝒢 G M A L A = A L A mid 𝒢 G M A
179 177 178 eqtr4d φ A M A A L M A = A mid 𝒢 G M A L A
180 160 179 breqtrd φ A M A D 𝒢 G A mid 𝒢 G M A L A
181 1 2 3 7 152 153 154 155 180 perpdrag φ A M A ⟨“ ZA mid 𝒢 G M A A ”⟩ 𝒢 G
182 151 181 pm2.61dane φ ⟨“ ZA mid 𝒢 G M A A ”⟩ 𝒢 G
183 1 2 3 7 21 4 19 15 9 israg φ ⟨“ ZA mid 𝒢 G M A A ”⟩ 𝒢 G Z - ˙ A = Z - ˙ pInv 𝒢 G A mid 𝒢 G M A A
184 182 183 mpbid φ Z - ˙ A = Z - ˙ pInv 𝒢 G A mid 𝒢 G M A A
185 eqidd φ A mid 𝒢 G M A = A mid 𝒢 G M A
186 1 2 3 4 5 9 14 21 15 ismidb φ M A = pInv 𝒢 G A mid 𝒢 G M A A A mid 𝒢 G M A = A mid 𝒢 G M A
187 185 186 mpbird φ M A = pInv 𝒢 G A mid 𝒢 G M A A
188 187 oveq2d φ Z - ˙ M A = Z - ˙ pInv 𝒢 G A mid 𝒢 G M A A
189 184 188 eqtr4d φ Z - ˙ A = Z - ˙ M A
190 1 2 3 7 21 4 19 11 9 mircgr φ Z - ˙ S A = Z - ˙ A
191 1 2 3 7 21 4 19 11 14 mircgr φ Z - ˙ S M A = Z - ˙ M A
192 189 190 191 3eqtr4d φ Z - ˙ S A = Z - ˙ S M A
193 192 adantr φ S A Z Z - ˙ S A = Z - ˙ S M A
194 1 2 3 125 127 126 127 130 193 tgcgrcomlr φ S A Z S A - ˙ Z = S M A - ˙ Z
195 189 adantr φ S A Z Z - ˙ A = Z - ˙ M A
196 11 fveq1i S A mid 𝒢 G M A = pInv 𝒢 G Z A mid 𝒢 G M A
197 1 2 3 4 5 9 14 11 19 mirmid φ S A mid 𝒢 G S M A = S A mid 𝒢 G M A
198 12 eqcomi A mid 𝒢 G M A mid 𝒢 G B mid 𝒢 G M B = Z
199 1 2 3 4 5 15 17 21 19 ismidb φ B mid 𝒢 G M B = pInv 𝒢 G Z A mid 𝒢 G M A A mid 𝒢 G M A mid 𝒢 G B mid 𝒢 G M B = Z
200 198 199 mpbiri φ B mid 𝒢 G M B = pInv 𝒢 G Z A mid 𝒢 G M A
201 196 197 200 3eqtr4a φ S A mid 𝒢 G S M A = B mid 𝒢 G M B
202 1 2 3 4 5 22 129 21 17 ismidb φ S M A = pInv 𝒢 G B mid 𝒢 G M B S A S A mid 𝒢 G S M A = B mid 𝒢 G M B
203 201 202 mpbird φ S M A = pInv 𝒢 G B mid 𝒢 G M B S A
204 119 203 oveq12d φ M B - ˙ S M A = pInv 𝒢 G B mid 𝒢 G M B B - ˙ pInv 𝒢 G B mid 𝒢 G M B S A
205 eqid pInv 𝒢 G B mid 𝒢 G M B = pInv 𝒢 G B mid 𝒢 G M B
206 1 2 3 7 21 4 17 205 10 22 miriso φ pInv 𝒢 G B mid 𝒢 G M B B - ˙ pInv 𝒢 G B mid 𝒢 G M B S A = B - ˙ S A
207 204 206 eqtr2d φ B - ˙ S A = M B - ˙ S M A
208 207 adantr φ S A Z B - ˙ S A = M B - ˙ S M A
209 1 2 3 125 132 126 133 130 208 tgcgrcomlr φ S A Z S A - ˙ B = S M A - ˙ M B
210 121 adantr φ S A Z Z - ˙ B = Z - ˙ M B
211 1 2 3 125 126 127 128 130 127 131 132 133 134 135 136 194 195 209 210 axtg5seg φ S A Z A - ˙ B = M A - ˙ M B
212 211 eqcomd φ S A Z M A - ˙ M B = A - ˙ B
213 124 212 pm2.61dane φ M A - ˙ M B = A - ˙ B