Step |
Hyp |
Ref |
Expression |
1 |
|
isfld |
|
2 |
1
|
simplbi |
|
3 |
|
drngring |
|
4 |
2 3
|
syl |
|
5 |
|
eqid |
|
6 |
5
|
frlmlmod |
|
7 |
6
|
adantlr |
|
8 |
|
simpr |
|
9 |
|
eldifi |
|
10 |
|
eqid |
|
11 |
5 10
|
frlmfibas |
|
12 |
9 11
|
sylan2 |
|
13 |
|
fvex |
|
14 |
|
curf |
|
15 |
13 14
|
mp3an3 |
|
16 |
|
feq3 |
|
17 |
16
|
biimpa |
|
18 |
12 15 17
|
syl2an |
|
19 |
18
|
anandirs |
|
20 |
|
eqid |
|
21 |
|
eqid |
|
22 |
|
eqid |
|
23 |
|
eqid |
|
24 |
|
eqid |
|
25 |
|
eqid |
|
26 |
20 21 22 23 24 25
|
islindf4 |
|
27 |
7 8 19 26
|
syl3anc |
|
28 |
5
|
frlmsca |
|
29 |
28
|
fvoveq1d |
|
30 |
12 29
|
eqtrd |
|
31 |
30
|
adantlr |
|
32 |
|
elmapi |
|
33 |
|
ffn |
|
34 |
33
|
adantl |
|
35 |
19
|
ffnd |
|
36 |
35
|
adantr |
|
37 |
|
simplr |
|
38 |
|
inidm |
|
39 |
|
eqidd |
|
40 |
|
eqidd |
|
41 |
34 36 37 37 38 39 40
|
offval |
|
42 |
|
simpllr |
|
43 |
|
ffvelrn |
|
44 |
43
|
adantll |
|
45 |
19
|
ffvelrnda |
|
46 |
45
|
adantlr |
|
47 |
|
eqid |
|
48 |
5 20 10 42 44 46 22 47
|
frlmvscafval |
|
49 |
|
fvex |
|
50 |
|
fnconstg |
|
51 |
49 50
|
mp1i |
|
52 |
15
|
ffvelrnda |
|
53 |
|
elmapfn |
|
54 |
52 53
|
syl |
|
55 |
54
|
adantlll |
|
56 |
55
|
adantlr |
|
57 |
49
|
fvconst2 |
|
58 |
57
|
adantl |
|
59 |
|
ffn |
|
60 |
59
|
anim2i |
|
61 |
60
|
ancoms |
|
62 |
61
|
ad4ant23 |
|
63 |
|
curfv |
|
64 |
63
|
3exp1 |
|
65 |
64
|
com4r |
|
66 |
65
|
imp41 |
|
67 |
62 66
|
sylanl1 |
|
68 |
51 56 42 42 38 58 67
|
offval |
|
69 |
48 68
|
eqtrd |
|
70 |
69
|
mpteq2dva |
|
71 |
41 70
|
eqtrd |
|
72 |
71
|
oveq2d |
|
73 |
|
simplll |
|
74 |
|
simp-4l |
|
75 |
43
|
ad4ant23 |
|
76 |
|
fovrn |
|
77 |
76
|
ad5ant245 |
|
78 |
10 47
|
ringcl |
|
79 |
74 75 77 78
|
syl3anc |
|
80 |
79
|
fmpttd |
|
81 |
80
|
adantllr |
|
82 |
|
elmapg |
|
83 |
13 82
|
mpan |
|
84 |
83
|
adantl |
|
85 |
12
|
eleq2d |
|
86 |
84 85
|
bitr3d |
|
87 |
86
|
ad5ant13 |
|
88 |
81 87
|
mpbid |
|
89 |
|
mptexg |
|
90 |
89
|
ralrimivw |
|
91 |
|
eqid |
|
92 |
91
|
fnmpt |
|
93 |
90 92
|
syl |
|
94 |
|
fvexd |
|
95 |
93 9 94
|
fndmfifsupp |
|
96 |
95
|
ad2antlr |
|
97 |
5 20 23 37 37 73 88 96
|
frlmgsum |
|
98 |
72 97
|
eqtr2d |
|
99 |
32 98
|
sylan2 |
|
100 |
|
eqid |
|
101 |
5 100
|
frlm0 |
|
102 |
101
|
ad4ant13 |
|
103 |
99 102
|
eqeq12d |
|
104 |
28
|
fveq2d |
|
105 |
104
|
sneqd |
|
106 |
105
|
xpeq2d |
|
107 |
106
|
eqeq2d |
|
108 |
107
|
ad4ant13 |
|
109 |
103 108
|
imbi12d |
|
110 |
31 109
|
raleqbidva |
|
111 |
27 110
|
bitr4d |
|
112 |
111
|
notbid |
|
113 |
|
rexanali |
|
114 |
112 113
|
bitr4di |
|
115 |
4 114
|
sylanl1 |
|
116 |
|
fconstfv |
|
117 |
|
fvex |
|
118 |
117
|
fconst2 |
|
119 |
116 118
|
sylbb1 |
|
120 |
119
|
ex |
|
121 |
120
|
con3d |
|
122 |
|
df-ne |
|
123 |
122
|
rexbii |
|
124 |
|
rexnal |
|
125 |
123 124
|
bitri |
|
126 |
121 125
|
syl6ibr |
|
127 |
33 126
|
syl |
|
128 |
127
|
adantl |
|
129 |
|
neldifsn |
|
130 |
|
difss |
|
131 |
|
diffi |
|
132 |
131
|
ad4antlr |
|
133 |
|
eleq2 |
|
134 |
133
|
notbid |
|
135 |
|
sseq1 |
|
136 |
134 135
|
anbi12d |
|
137 |
136
|
anbi2d |
|
138 |
|
mpteq1 |
|
139 |
|
mpt0 |
|
140 |
138 139
|
eqtrdi |
|
141 |
140
|
oveq2d |
|
142 |
100
|
gsum0 |
|
143 |
141 142
|
eqtrdi |
|
144 |
143
|
oveq1d |
|
145 |
144
|
ifeq1d |
|
146 |
145
|
mpoeq3dv |
|
147 |
146
|
fveq2d |
|
148 |
147
|
eqeq2d |
|
149 |
137 148
|
imbi12d |
|
150 |
|
elequ2 |
|
151 |
150
|
notbid |
|
152 |
|
sseq1 |
|
153 |
151 152
|
anbi12d |
|
154 |
153
|
anbi2d |
|
155 |
|
mpteq1 |
|
156 |
155
|
oveq2d |
|
157 |
156
|
oveq1d |
|
158 |
157
|
ifeq1d |
|
159 |
158
|
mpoeq3dv |
|
160 |
159
|
fveq2d |
|
161 |
160
|
eqeq2d |
|
162 |
154 161
|
imbi12d |
|
163 |
|
eleq2 |
|
164 |
163
|
notbid |
|
165 |
|
sseq1 |
|
166 |
164 165
|
anbi12d |
|
167 |
166
|
anbi2d |
|
168 |
|
mpteq1 |
|
169 |
168
|
oveq2d |
|
170 |
169
|
oveq1d |
|
171 |
170
|
ifeq1d |
|
172 |
171
|
mpoeq3dv |
|
173 |
172
|
fveq2d |
|
174 |
173
|
eqeq2d |
|
175 |
167 174
|
imbi12d |
|
176 |
|
eleq2 |
|
177 |
176
|
notbid |
|
178 |
|
sseq1 |
|
179 |
177 178
|
anbi12d |
|
180 |
179
|
anbi2d |
|
181 |
|
mpteq1 |
|
182 |
181
|
oveq2d |
|
183 |
182
|
oveq1d |
|
184 |
183
|
ifeq1d |
|
185 |
184
|
mpoeq3dv |
|
186 |
185
|
fveq2d |
|
187 |
186
|
eqeq2d |
|
188 |
180 187
|
imbi12d |
|
189 |
|
fnov |
|
190 |
59 189
|
sylib |
|
191 |
190
|
adantl |
|
192 |
|
ringgrp |
|
193 |
4 192
|
syl |
|
194 |
|
oveq1 |
|
195 |
194
|
equcoms |
|
196 |
195
|
oveq2d |
|
197 |
|
simp1l |
|
198 |
|
fovrn |
|
199 |
198
|
3adant1l |
|
200 |
|
eqid |
|
201 |
10 200 100
|
grplid |
|
202 |
197 199 201
|
syl2anc |
|
203 |
196 202
|
sylan9eqr |
|
204 |
|
eqidd |
|
205 |
203 204
|
ifeqda |
|
206 |
205
|
mpoeq3dva |
|
207 |
193 206
|
sylan |
|
208 |
191 207
|
eqtr4d |
|
209 |
208
|
fveq2d |
|
210 |
209
|
ad4antr |
|
211 |
|
elun1 |
|
212 |
211
|
con3i |
|
213 |
|
ssun1 |
|
214 |
|
sstr |
|
215 |
213 214
|
mpan |
|
216 |
212 215
|
anim12i |
|
217 |
216
|
anim2i |
|
218 |
217
|
adantr |
|
219 |
|
velsn |
|
220 |
|
elun2 |
|
221 |
219 220
|
sylbir |
|
222 |
221
|
necon3bi |
|
223 |
222
|
anim1i |
|
224 |
|
ringcmn |
|
225 |
4 224
|
syl |
|
226 |
225
|
ad7antr |
|
227 |
|
simplr |
|
228 |
215
|
adantl |
|
229 |
|
ssfi |
|
230 |
227 228 229
|
syl2an |
|
231 |
230
|
ad5ant13 |
|
232 |
215
|
sselda |
|
233 |
232
|
adantll |
|
234 |
233
|
ad4ant24 |
|
235 |
4
|
ad6antr |
|
236 |
2
|
ad2antrr |
|
237 |
|
ffvelrn |
|
238 |
237
|
anim2i |
|
239 |
238
|
anassrs |
|
240 |
|
eqid |
|
241 |
10 100 240
|
drnginvrcl |
|
242 |
241
|
3expa |
|
243 |
239 242
|
sylan |
|
244 |
243
|
anasss |
|
245 |
236 244
|
sylanl1 |
|
246 |
245
|
ad2antrr |
|
247 |
43
|
ad5ant25 |
|
248 |
|
simp-4r |
|
249 |
76
|
3expa |
|
250 |
249
|
an32s |
|
251 |
248 250
|
sylanl1 |
|
252 |
235 247 251 78
|
syl3anc |
|
253 |
10 47
|
ringcl |
|
254 |
235 246 252 253
|
syl3anc |
|
255 |
254
|
adantllr |
|
256 |
234 255
|
syldan |
|
257 |
256
|
adantllr |
|
258 |
|
vex |
|
259 |
258
|
a1i |
|
260 |
|
simplr |
|
261 |
|
ssun2 |
|
262 |
|
sstr |
|
263 |
261 262
|
mpan |
|
264 |
258
|
snss |
|
265 |
263 264
|
sylibr |
|
266 |
265
|
adantl |
|
267 |
4
|
ad6antr |
|
268 |
4
|
ad5antr |
|
269 |
245
|
adantr |
|
270 |
|
ffvelrn |
|
271 |
270
|
ad4ant24 |
|
272 |
10 47
|
ringcl |
|
273 |
268 269 271 272
|
syl3anc |
|
274 |
273
|
adantr |
|
275 |
|
fovrn |
|
276 |
275
|
3expa |
|
277 |
248 276
|
sylanl1 |
|
278 |
10 47
|
ringcl |
|
279 |
267 274 277 278
|
syl3anc |
|
280 |
266 279
|
sylanl2 |
|
281 |
280
|
adantlr |
|
282 |
|
fveq2 |
|
283 |
|
oveq1 |
|
284 |
282 283
|
oveq12d |
|
285 |
284
|
oveq2d |
|
286 |
245
|
ad2antrr |
|
287 |
270
|
ad5ant24 |
|
288 |
10 47
|
ringass |
|
289 |
267 286 287 277 288
|
syl13anc |
|
290 |
289
|
eqcomd |
|
291 |
266 290
|
sylanl2 |
|
292 |
285 291
|
sylan9eqr |
|
293 |
292
|
adantllr |
|
294 |
10 200 226 231 257 259 260 281 293
|
gsumunsnd |
|
295 |
294
|
oveq1d |
|
296 |
|
ringabl |
|
297 |
4 296
|
syl |
|
298 |
297
|
ad6antr |
|
299 |
225
|
ad6antr |
|
300 |
|
vex |
|
301 |
300
|
a1i |
|
302 |
|
ssel2 |
|
303 |
302 254
|
sylan2 |
|
304 |
303
|
anassrs |
|
305 |
304
|
fmpttd |
|
306 |
305
|
an32s |
|
307 |
|
ovex |
|
308 |
|
eqid |
|
309 |
307 308
|
fnmpti |
|
310 |
309
|
a1i |
|
311 |
|
fvexd |
|
312 |
310 229 311
|
fndmfifsupp |
|
313 |
312
|
adantll |
|
314 |
313
|
ad5ant14 |
|
315 |
10 100 299 301 306 314
|
gsumcl |
|
316 |
215 315
|
sylanl2 |
|
317 |
265 279
|
sylanl2 |
|
318 |
|
simpllr |
|
319 |
|
simpl |
|
320 |
318 319
|
anim12i |
|
321 |
320
|
adantr |
|
322 |
|
fovrn |
|
323 |
322
|
3expa |
|
324 |
321 323
|
sylan |
|
325 |
10 200 298 316 317 324
|
abl32 |
|
326 |
325
|
adantlrl |
|
327 |
326
|
adantlr |
|
328 |
295 327
|
eqtrd |
|
329 |
328
|
ifeq1d |
|
330 |
329
|
3adant2 |
|
331 |
330
|
mpoeq3dva |
|
332 |
331
|
fveq2d |
|
333 |
|
eqid |
|
334 |
1
|
simprbi |
|
335 |
334
|
ad5antr |
|
336 |
|
simp-4r |
|
337 |
193
|
ad6antr |
|
338 |
320
|
adantr |
|
339 |
338 323
|
sylan |
|
340 |
10 200
|
grpcl |
|
341 |
337 315 339 340
|
syl3anc |
|
342 |
228 341
|
sylanl2 |
|
343 |
248 266
|
anim12i |
|
344 |
343 276
|
sylan |
|
345 |
|
simp-5r |
|
346 |
345 198
|
syl3an1 |
|
347 |
266 273
|
sylan2 |
|
348 |
|
simplrl |
|
349 |
265
|
ad2antll |
|
350 |
|
simprl |
|
351 |
333 10 200 47 335 336 342 344 346 347 348 349 350
|
mdetero |
|
352 |
351
|
adantr |
|
353 |
332 352
|
eqtrd |
|
354 |
|
iftrue |
|
355 |
|
oveq1 |
|
356 |
354 355
|
eqtr4d |
|
357 |
|
iffalse |
|
358 |
356 357
|
pm2.61i |
|
359 |
|
ifeq2 |
|
360 |
358 359
|
mp1i |
|
361 |
360
|
mpoeq3ia |
|
362 |
361
|
fveq2i |
|
363 |
|
ifeq2 |
|
364 |
358 363
|
mp1i |
|
365 |
364
|
mpoeq3ia |
|
366 |
365
|
fveq2i |
|
367 |
353 362 366
|
3eqtr3g |
|
368 |
223 367
|
sylanl2 |
|
369 |
368
|
eqeq2d |
|
370 |
369
|
biimprd |
|
371 |
218 370
|
embantd |
|
372 |
371
|
expcom |
|
373 |
372
|
com23 |
|
374 |
373
|
adantl |
|
375 |
149 162 175 188 210 374
|
findcard2s |
|
376 |
132 375
|
mpcom |
|
377 |
129 130 376
|
mpanr12 |
|
378 |
377
|
adantlr |
|
379 |
|
eqid |
|
380 |
|
fconstmpt |
|
381 |
380
|
eqeq2i |
|
382 |
|
ovex |
|
383 |
382
|
rgenw |
|
384 |
|
mpteqb |
|
385 |
383 384
|
ax-mp |
|
386 |
381 385
|
bitri |
|
387 |
225
|
ad5antr |
|
388 |
|
simp-4r |
|
389 |
|
eqid |
|
390 |
307 389
|
fnmpti |
|
391 |
390
|
a1i |
|
392 |
|
id |
|
393 |
|
fvexd |
|
394 |
391 392 393
|
fndmfifsupp |
|
395 |
394
|
ad4antlr |
|
396 |
|
simplrl |
|
397 |
320 323
|
sylan |
|
398 |
|
fveq2 |
|
399 |
|
oveq1 |
|
400 |
398 399
|
oveq12d |
|
401 |
400
|
oveq2d |
|
402 |
|
simpll |
|
403 |
2 237
|
anim12i |
|
404 |
403
|
anassrs |
|
405 |
|
eqid |
|
406 |
10 100 47 405 240
|
drnginvrl |
|
407 |
406
|
3expa |
|
408 |
404 407
|
sylan |
|
409 |
408
|
anasss |
|
410 |
409
|
oveq1d |
|
411 |
402 410
|
sylanl1 |
|
412 |
411
|
adantr |
|
413 |
4
|
ad5antr |
|
414 |
245
|
adantr |
|
415 |
237
|
ad2ant2lr |
|
416 |
415
|
adantr |
|
417 |
10 47
|
ringass |
|
418 |
413 414 416 397 417
|
syl13anc |
|
419 |
4
|
adantr |
|
420 |
419
|
3ad2ant1 |
|
421 |
322
|
3adant1l |
|
422 |
10 47 405
|
ringlidm |
|
423 |
420 421 422
|
syl2anc |
|
424 |
423
|
ad5ant145 |
|
425 |
424
|
adantlrr |
|
426 |
412 418 425
|
3eqtr3d |
|
427 |
401 426
|
sylan9eqr |
|
428 |
10 200 387 388 395 254 396 397 427
|
gsumdifsnd |
|
429 |
|
ovex |
|
430 |
|
eqid |
|
431 |
429 430
|
fnmpti |
|
432 |
431
|
a1i |
|
433 |
432 392 393
|
fndmfifsupp |
|
434 |
433
|
ad4antlr |
|
435 |
10 100 200 47 413 388 414 252 434
|
gsummulc2 |
|
436 |
428 435
|
eqtr3d |
|
437 |
436
|
adantr |
|
438 |
|
oveq2 |
|
439 |
438
|
adantl |
|
440 |
4
|
ad4antr |
|
441 |
10 47 100
|
ringrz |
|
442 |
440 245 441
|
syl2anc |
|
443 |
442
|
ad2antrr |
|
444 |
437 439 443
|
3eqtrd |
|
445 |
444
|
ifeq1d |
|
446 |
445
|
ex |
|
447 |
446
|
ralimdva |
|
448 |
447
|
imp |
|
449 |
386 448
|
sylan2b |
|
450 |
449 379
|
jctil |
|
451 |
450
|
ralrimivw |
|
452 |
|
mpoeq123 |
|
453 |
379 451 452
|
sylancr |
|
454 |
453
|
an32s |
|
455 |
454
|
fveq2d |
|
456 |
334
|
ad3antrrr |
|
457 |
|
simplr |
|
458 |
|
simpllr |
|
459 |
458 198
|
syl3an1 |
|
460 |
|
simprl |
|
461 |
333 10 100 456 457 459 460
|
mdetr0 |
|
462 |
461
|
ad4ant14 |
|
463 |
378 455 462
|
3eqtrd |
|
464 |
463
|
rexlimdvaa |
|
465 |
464
|
expimpd |
|
466 |
128 465
|
sylan2d |
|
467 |
32 466
|
sylan2 |
|
468 |
467
|
rexlimdva |
|
469 |
9 468
|
sylan2 |
|
470 |
115 469
|
sylbid |
|