Step |
Hyp |
Ref |
Expression |
1 |
|
evlslem1.p |
|
2 |
|
evlslem1.b |
|
3 |
|
evlslem1.c |
|
4 |
|
evlslem1.d |
|
5 |
|
evlslem1.t |
|
6 |
|
evlslem1.x |
|
7 |
|
evlslem1.m |
|
8 |
|
evlslem1.v |
|
9 |
|
evlslem1.e |
|
10 |
|
evlslem1.i |
|
11 |
|
evlslem1.r |
|
12 |
|
evlslem1.s |
|
13 |
|
evlslem1.f |
|
14 |
|
evlslem1.g |
|
15 |
|
evlslem1.a |
|
16 |
|
eqid |
|
17 |
|
eqid |
|
18 |
|
eqid |
|
19 |
11
|
crngringd |
|
20 |
1 10 19
|
mplringd |
|
21 |
12
|
crngringd |
|
22 |
|
2fveq3 |
|
23 |
|
fveq2 |
|
24 |
22 23
|
eqeq12d |
|
25 |
|
eqid |
|
26 |
|
eqid |
|
27 |
10
|
adantr |
|
28 |
19
|
adantr |
|
29 |
|
simpr |
|
30 |
1 4 25 26 15 27 28 29
|
mplascl |
|
31 |
30
|
fveq2d |
|
32 |
11
|
adantr |
|
33 |
12
|
adantr |
|
34 |
13
|
adantr |
|
35 |
14
|
adantr |
|
36 |
4
|
psrbag0 |
|
37 |
10 36
|
syl |
|
38 |
37
|
adantr |
|
39 |
1 2 3 26 4 5 6 7 8 9 27 32 33 34 35 25 38 29
|
evlslem3 |
|
40 |
|
0zd |
|
41 |
|
fvexd |
|
42 |
|
fconstmpt |
|
43 |
42
|
a1i |
|
44 |
14
|
feqmptd |
|
45 |
10 40 41 43 44
|
offval2 |
|
46 |
14
|
ffvelcdmda |
|
47 |
5 3
|
mgpbas |
|
48 |
5 17
|
ringidval |
|
49 |
47 48 6
|
mulg0 |
|
50 |
46 49
|
syl |
|
51 |
50
|
mpteq2dva |
|
52 |
45 51
|
eqtrd |
|
53 |
52
|
oveq2d |
|
54 |
5
|
crngmgp |
|
55 |
12 54
|
syl |
|
56 |
55
|
cmnmndd |
|
57 |
48
|
gsumz |
|
58 |
56 10 57
|
syl2anc |
|
59 |
53 58
|
eqtrd |
|
60 |
59
|
adantr |
|
61 |
60
|
oveq2d |
|
62 |
26 3
|
rhmf |
|
63 |
13 62
|
syl |
|
64 |
63
|
ffvelcdmda |
|
65 |
3 7 17
|
ringridm |
|
66 |
21 64 65
|
syl2an2r |
|
67 |
61 66
|
eqtrd |
|
68 |
31 39 67
|
3eqtrd |
|
69 |
68
|
ralrimiva |
|
70 |
|
eqid |
|
71 |
26 70
|
ringidcl |
|
72 |
19 71
|
syl |
|
73 |
24 69 72
|
rspcdva |
|
74 |
1
|
mplassa |
|
75 |
10 11 74
|
syl2anc |
|
76 |
|
eqid |
|
77 |
15 76
|
asclrhm |
|
78 |
75 77
|
syl |
|
79 |
1 10 11
|
mplsca |
|
80 |
79
|
oveq1d |
|
81 |
78 80
|
eleqtrrd |
|
82 |
70 16
|
rhm1 |
|
83 |
81 82
|
syl |
|
84 |
83
|
fveq2d |
|
85 |
70 17
|
rhm1 |
|
86 |
13 85
|
syl |
|
87 |
73 84 86
|
3eqtr3d |
|
88 |
|
eqid |
|
89 |
|
eqid |
|
90 |
20
|
ringgrpd |
|
91 |
21
|
ringgrpd |
|
92 |
|
eqid |
|
93 |
|
ringcmn |
|
94 |
21 93
|
syl |
|
95 |
94
|
adantr |
|
96 |
|
ovex |
|
97 |
4 96
|
rabex2 |
|
98 |
97
|
a1i |
|
99 |
10
|
adantr |
|
100 |
11
|
adantr |
|
101 |
12
|
adantr |
|
102 |
13
|
adantr |
|
103 |
14
|
adantr |
|
104 |
|
simpr |
|
105 |
1 2 3 4 5 6 7 8 9 99 100 101 102 103 104
|
evlslem6 |
|
106 |
105
|
simpld |
|
107 |
105
|
simprd |
|
108 |
3 92 95 98 106 107
|
gsumcl |
|
109 |
108 9
|
fmptd |
|
110 |
|
eqid |
|
111 |
|
simplrl |
|
112 |
|
simplrr |
|
113 |
1 2 110 88 111 112
|
mpladd |
|
114 |
113
|
fveq1d |
|
115 |
|
simprl |
|
116 |
1 26 2 4 115
|
mplelf |
|
117 |
116
|
ffnd |
|
118 |
117
|
adantr |
|
119 |
|
simprr |
|
120 |
1 26 2 4 119
|
mplelf |
|
121 |
120
|
ffnd |
|
122 |
121
|
adantr |
|
123 |
97
|
a1i |
|
124 |
|
simpr |
|
125 |
|
fnfvof |
|
126 |
118 122 123 124 125
|
syl22anc |
|
127 |
114 126
|
eqtrd |
|
128 |
127
|
fveq2d |
|
129 |
|
rhmghm |
|
130 |
13 129
|
syl |
|
131 |
130
|
ad2antrr |
|
132 |
116
|
ffvelcdmda |
|
133 |
120
|
ffvelcdmda |
|
134 |
26 110 89
|
ghmlin |
|
135 |
131 132 133 134
|
syl3anc |
|
136 |
128 135
|
eqtrd |
|
137 |
136
|
oveq1d |
|
138 |
21
|
ad2antrr |
|
139 |
63
|
ad2antrr |
|
140 |
139 132
|
ffvelcdmd |
|
141 |
139 133
|
ffvelcdmd |
|
142 |
55
|
ad2antrr |
|
143 |
14
|
ad2antrr |
|
144 |
4 47 6 142 124 143
|
psrbagev2 |
|
145 |
3 89 7
|
ringdir |
|
146 |
138 140 141 144 145
|
syl13anc |
|
147 |
137 146
|
eqtrd |
|
148 |
147
|
mpteq2dva |
|
149 |
97
|
a1i |
|
150 |
|
ovexd |
|
151 |
|
ovexd |
|
152 |
|
eqidd |
|
153 |
|
eqidd |
|
154 |
149 150 151 152 153
|
offval2 |
|
155 |
148 154
|
eqtr4d |
|
156 |
155
|
oveq2d |
|
157 |
94
|
adantr |
|
158 |
10
|
adantr |
|
159 |
11
|
adantr |
|
160 |
12
|
adantr |
|
161 |
13
|
adantr |
|
162 |
14
|
adantr |
|
163 |
1 2 3 4 5 6 7 8 9 158 159 160 161 162 115
|
evlslem6 |
|
164 |
163
|
simpld |
|
165 |
1 2 3 4 5 6 7 8 9 158 159 160 161 162 119
|
evlslem6 |
|
166 |
165
|
simpld |
|
167 |
163
|
simprd |
|
168 |
165
|
simprd |
|
169 |
3 92 89 157 149 164 166 167 168
|
gsumadd |
|
170 |
156 169
|
eqtrd |
|
171 |
90
|
adantr |
|
172 |
2 88
|
grpcl |
|
173 |
171 115 119 172
|
syl3anc |
|
174 |
|
fveq1 |
|
175 |
174
|
fveq2d |
|
176 |
175
|
oveq1d |
|
177 |
176
|
mpteq2dv |
|
178 |
177
|
oveq2d |
|
179 |
|
ovex |
|
180 |
178 9 179
|
fvmpt |
|
181 |
173 180
|
syl |
|
182 |
|
fveq1 |
|
183 |
182
|
fveq2d |
|
184 |
183
|
oveq1d |
|
185 |
184
|
mpteq2dv |
|
186 |
185
|
oveq2d |
|
187 |
|
ovex |
|
188 |
186 9 187
|
fvmpt |
|
189 |
115 188
|
syl |
|
190 |
|
fveq1 |
|
191 |
190
|
fveq2d |
|
192 |
191
|
oveq1d |
|
193 |
192
|
mpteq2dv |
|
194 |
193
|
oveq2d |
|
195 |
|
ovex |
|
196 |
194 9 195
|
fvmpt |
|
197 |
196
|
ad2antll |
|
198 |
189 197
|
oveq12d |
|
199 |
170 181 198
|
3eqtr4d |
|
200 |
2 3 88 89 90 91 109 199
|
isghmd |
|
201 |
|
eqid |
|
202 |
201 5
|
rhmmhm |
|
203 |
13 202
|
syl |
|
204 |
203
|
adantr |
|
205 |
|
simprll |
|
206 |
1 26 2 4 205
|
mplelf |
|
207 |
|
simprrl |
|
208 |
206 207
|
ffvelcdmd |
|
209 |
|
simprlr |
|
210 |
1 26 2 4 209
|
mplelf |
|
211 |
|
simprrr |
|
212 |
210 211
|
ffvelcdmd |
|
213 |
201 26
|
mgpbas |
|
214 |
|
eqid |
|
215 |
201 214
|
mgpplusg |
|
216 |
5 7
|
mgpplusg |
|
217 |
213 215 216
|
mhmlin |
|
218 |
204 208 212 217
|
syl3anc |
|
219 |
56
|
ad2antrr |
|
220 |
|
simprl |
|
221 |
4
|
psrbagf |
|
222 |
220 221
|
syl |
|
223 |
222
|
ffvelcdmda |
|
224 |
4
|
psrbagf |
|
225 |
224
|
ad2antll |
|
226 |
225
|
ffvelcdmda |
|
227 |
14
|
adantr |
|
228 |
227
|
ffvelcdmda |
|
229 |
47 6 216
|
mulgnn0dir |
|
230 |
219 223 226 228 229
|
syl13anc |
|
231 |
230
|
mpteq2dva |
|
232 |
10
|
adantr |
|
233 |
|
ovexd |
|
234 |
|
fvexd |
|
235 |
222
|
ffnd |
|
236 |
225
|
ffnd |
|
237 |
|
inidm |
|
238 |
|
eqidd |
|
239 |
|
eqidd |
|
240 |
235 236 232 232 237 238 239
|
offval |
|
241 |
14
|
feqmptd |
|
242 |
241
|
adantr |
|
243 |
232 233 234 240 242
|
offval2 |
|
244 |
|
ovexd |
|
245 |
|
ovexd |
|
246 |
14
|
ffnd |
|
247 |
246
|
adantr |
|
248 |
|
eqidd |
|
249 |
235 247 232 232 237 238 248
|
offval |
|
250 |
236 247 232 232 237 239 248
|
offval |
|
251 |
232 244 245 249 250
|
offval2 |
|
252 |
231 243 251
|
3eqtr4d |
|
253 |
252
|
oveq2d |
|
254 |
55
|
adantr |
|
255 |
4 47 6 48 254 220 227
|
psrbagev1 |
|
256 |
255
|
simpld |
|
257 |
|
simprr |
|
258 |
4 47 6 48 254 257 227
|
psrbagev1 |
|
259 |
258
|
simpld |
|
260 |
255
|
simprd |
|
261 |
258
|
simprd |
|
262 |
47 48 216 254 232 256 259 260 261
|
gsumadd |
|
263 |
253 262
|
eqtrd |
|
264 |
263
|
adantrl |
|
265 |
218 264
|
oveq12d |
|
266 |
55
|
adantr |
|
267 |
63
|
adantr |
|
268 |
267 208
|
ffvelcdmd |
|
269 |
267 212
|
ffvelcdmd |
|
270 |
4 47 6 254 220 227
|
psrbagev2 |
|
271 |
270
|
adantrl |
|
272 |
4 47 6 254 257 227
|
psrbagev2 |
|
273 |
272
|
adantrl |
|
274 |
47 216
|
cmn4 |
|
275 |
266 268 269 271 273 274
|
syl122anc |
|
276 |
265 275
|
eqtrd |
|
277 |
10
|
adantr |
|
278 |
11
|
adantr |
|
279 |
12
|
adantr |
|
280 |
13
|
adantr |
|
281 |
14
|
adantr |
|
282 |
4
|
psrbagaddcl |
|
283 |
282
|
ad2antll |
|
284 |
19
|
adantr |
|
285 |
26 214
|
ringcl |
|
286 |
284 208 212 285
|
syl3anc |
|
287 |
1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 283 286
|
evlslem3 |
|
288 |
1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 207 208
|
evlslem3 |
|
289 |
1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 211 212
|
evlslem3 |
|
290 |
288 289
|
oveq12d |
|
291 |
276 287 290
|
3eqtr4d |
|
292 |
1 2 7 25 4 10 11 12 200 291
|
evlslem2 |
|
293 |
2 16 17 18 7 20 21 87 292 3 88 89 109 199
|
isrhmd |
|
294 |
|
ovex |
|
295 |
294 9
|
fnmpti |
|
296 |
295
|
a1i |
|
297 |
26 2
|
rhmf |
|
298 |
81 297
|
syl |
|
299 |
298
|
ffnd |
|
300 |
298
|
frnd |
|
301 |
|
fnco |
|
302 |
296 299 300 301
|
syl3anc |
|
303 |
63
|
ffnd |
|
304 |
|
fvco2 |
|
305 |
299 304
|
sylan |
|
306 |
305 68
|
eqtrd |
|
307 |
302 303 306
|
eqfnfvd |
|
308 |
1 8 2 10 19
|
mvrf2 |
|
309 |
308
|
ffnd |
|
310 |
308
|
frnd |
|
311 |
|
fnco |
|
312 |
296 309 310 311
|
syl3anc |
|
313 |
|
fvco2 |
|
314 |
309 313
|
sylan |
|
315 |
10
|
adantr |
|
316 |
11
|
adantr |
|
317 |
|
simpr |
|
318 |
8 4 25 70 315 316 317
|
mvrval |
|
319 |
318
|
fveq2d |
|
320 |
12
|
adantr |
|
321 |
13
|
adantr |
|
322 |
14
|
adantr |
|
323 |
4
|
psrbagsn |
|
324 |
10 323
|
syl |
|
325 |
324
|
adantr |
|
326 |
72
|
adantr |
|
327 |
1 2 3 26 4 5 6 7 8 9 315 316 320 321 322 25 325 326
|
evlslem3 |
|
328 |
86
|
adantr |
|
329 |
|
1nn0 |
|
330 |
|
0nn0 |
|
331 |
329 330
|
ifcli |
|
332 |
331
|
a1i |
|
333 |
14
|
ffvelcdmda |
|
334 |
|
eqidd |
|
335 |
14
|
feqmptd |
|
336 |
10 332 333 334 335
|
offval2 |
|
337 |
|
oveq1 |
|
338 |
337
|
eqeq1d |
|
339 |
|
oveq1 |
|
340 |
339
|
eqeq1d |
|
341 |
333
|
adantr |
|
342 |
47 6
|
mulg1 |
|
343 |
341 342
|
syl |
|
344 |
|
iftrue |
|
345 |
344
|
adantl |
|
346 |
343 345
|
eqtr4d |
|
347 |
47 48 6
|
mulg0 |
|
348 |
333 347
|
syl |
|
349 |
348
|
adantr |
|
350 |
|
iffalse |
|
351 |
350
|
adantl |
|
352 |
349 351
|
eqtr4d |
|
353 |
338 340 346 352
|
ifbothda |
|
354 |
353
|
mpteq2dva |
|
355 |
336 354
|
eqtrd |
|
356 |
355
|
adantr |
|
357 |
356
|
oveq2d |
|
358 |
56
|
adantr |
|
359 |
333
|
adantlr |
|
360 |
3 17
|
ringidcl |
|
361 |
21 360
|
syl |
|
362 |
361
|
ad2antrr |
|
363 |
359 362
|
ifcld |
|
364 |
363
|
fmpttd |
|
365 |
|
eldifsnneq |
|
366 |
365 350
|
syl |
|
367 |
366
|
adantl |
|
368 |
367 315
|
suppss2 |
|
369 |
47 48 358 315 317 364 368
|
gsumpt |
|
370 |
|
fveq2 |
|
371 |
344 370
|
eqtrd |
|
372 |
|
eqid |
|
373 |
|
fvex |
|
374 |
371 372 373
|
fvmpt |
|
375 |
374
|
adantl |
|
376 |
357 369 375
|
3eqtrd |
|
377 |
328 376
|
oveq12d |
|
378 |
3 7 17
|
ringlidm |
|
379 |
21 46 378
|
syl2an2r |
|
380 |
377 379
|
eqtrd |
|
381 |
319 327 380
|
3eqtrd |
|
382 |
314 381
|
eqtrd |
|
383 |
312 246 382
|
eqfnfvd |
|
384 |
293 307 383
|
3jca |
|