Step | Hyp | Ref
| Expression |
1 | | mplcoe1.p |
. . . . . 6
mPoly |
2 | | eqid 2622 |
. . . . . 6
|
3 | | mplcoe1.b |
. . . . . 6
|
4 | | mplcoe1.d |
. . . . . 6
|
5 | | mplcoe1.x |
. . . . . 6
|
6 | 1, 2, 3, 4, 5 | mplelf 19433 |
. . . . 5
|
7 | 6 | feqmptd 6249 |
. . . 4
|
8 | | iftrue 4092 |
. . . . . . 7
supp supp
|
9 | 8 | adantl 482 |
. . . . . 6
supp
supp |
10 | | eldif 3584 |
. . . . . . . 8
supp
supp |
11 | | ifid 4125 |
. . . . . . . . 9
supp |
12 | | ssid 3624 |
. . . . . . . . . . . 12
supp supp |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
supp supp |
14 | | ovex 6678 |
. . . . . . . . . . . . 13
|
15 | 4, 14 | rabex2 4815 |
. . . . . . . . . . . 12
|
16 | 15 | a1i 11 |
. . . . . . . . . . 11
|
17 | | mplcoe1.z |
. . . . . . . . . . . . 13
|
18 | | fvex 6201 |
. . . . . . . . . . . . 13
|
19 | 17, 18 | eqeltri 2697 |
. . . . . . . . . . . 12
|
20 | 19 | a1i 11 |
. . . . . . . . . . 11
|
21 | 6, 13, 16, 20 | suppssr 7326 |
. . . . . . . . . 10
supp |
22 | 21 | ifeq2d 4105 |
. . . . . . . . 9
supp supp
supp |
23 | 11, 22 | syl5reqr 2671 |
. . . . . . . 8
supp supp
|
24 | 10, 23 | sylan2br 493 |
. . . . . . 7
supp supp
|
25 | 24 | anassrs 680 |
. . . . . 6
supp supp
|
26 | 9, 25 | pm2.61dan 832 |
. . . . 5
supp
|
27 | 26 | mpteq2dva 4744 |
. . . 4
supp |
28 | 7, 27 | eqtr4d 2659 |
. . 3
supp |
29 | | suppssdm 7308 |
. . . . 5
supp |
30 | | fdm 6051 |
. . . . . 6
|
31 | 6, 30 | syl 17 |
. . . . 5
|
32 | 29, 31 | syl5sseq 3653 |
. . . 4
supp |
33 | | eqid 2622 |
. . . . . . . . 9
mPwSer mPwSer |
34 | | eqid 2622 |
. . . . . . . . 9
mPwSer mPwSer |
35 | 1, 33, 34, 17, 3 | mplelbas 19430 |
. . . . . . . 8
mPwSer finSupp |
36 | 35 | simprbi 480 |
. . . . . . 7
finSupp |
37 | 5, 36 | syl 17 |
. . . . . 6
finSupp
|
38 | 37 | fsuppimpd 8282 |
. . . . 5
supp |
39 | | sseq1 3626 |
. . . . . . . 8
|
40 | | mpteq1 4737 |
. . . . . . . . . . . 12
|
41 | | mpt0 6021 |
. . . . . . . . . . . 12
|
42 | 40, 41 | syl6eq 2672 |
. . . . . . . . . . 11
|
43 | 42 | oveq2d 6666 |
. . . . . . . . . 10
g g |
44 | | eqid 2622 |
. . . . . . . . . . 11
|
45 | 44 | gsum0 17278 |
. . . . . . . . . 10
g |
46 | 43, 45 | syl6eq 2672 |
. . . . . . . . 9
g |
47 | | noel 3919 |
. . . . . . . . . . . 12
|
48 | | eleq2 2690 |
. . . . . . . . . . . 12
|
49 | 47, 48 | mtbiri 317 |
. . . . . . . . . . 11
|
50 | 49 | iffalsed 4097 |
. . . . . . . . . 10
|
51 | 50 | mpteq2dv 4745 |
. . . . . . . . 9
|
52 | 46, 51 | eqeq12d 2637 |
. . . . . . . 8
g |
53 | 39, 52 | imbi12d 334 |
. . . . . . 7
g
|
54 | 53 | imbi2d 330 |
. . . . . 6
g
|
55 | | sseq1 3626 |
. . . . . . . 8
|
56 | | mpteq1 4737 |
. . . . . . . . . 10
|
57 | 56 | oveq2d 6666 |
. . . . . . . . 9
g g |
58 | | eleq2 2690 |
. . . . . . . . . . 11
|
59 | 58 | ifbid 4108 |
. . . . . . . . . 10
|
60 | 59 | mpteq2dv 4745 |
. . . . . . . . 9
|
61 | 57, 60 | eqeq12d 2637 |
. . . . . . . 8
g g |
62 | 55, 61 | imbi12d 334 |
. . . . . . 7
g
g
|
63 | 62 | imbi2d 330 |
. . . . . 6
g
g |
64 | | sseq1 3626 |
. . . . . . . 8
|
65 | | mpteq1 4737 |
. . . . . . . . . 10
|
66 | 65 | oveq2d 6666 |
. . . . . . . . 9
g g |
67 | | eleq2 2690 |
. . . . . . . . . . 11
|
68 | 67 | ifbid 4108 |
. . . . . . . . . 10
|
69 | 68 | mpteq2dv 4745 |
. . . . . . . . 9
|
70 | 66, 69 | eqeq12d 2637 |
. . . . . . . 8
g g |
71 | 64, 70 | imbi12d 334 |
. . . . . . 7
g
g |
72 | 71 | imbi2d 330 |
. . . . . 6
g
g |
73 | | sseq1 3626 |
. . . . . . . 8
supp supp |
74 | | mpteq1 4737 |
. . . . . . . . . 10
supp supp |
75 | 74 | oveq2d 6666 |
. . . . . . . . 9
supp g g supp
|
76 | | eleq2 2690 |
. . . . . . . . . . 11
supp supp
|
77 | 76 | ifbid 4108 |
. . . . . . . . . 10
supp supp |
78 | 77 | mpteq2dv 4745 |
. . . . . . . . 9
supp supp
|
79 | 75, 78 | eqeq12d 2637 |
. . . . . . . 8
supp g g supp supp |
80 | 73, 79 | imbi12d 334 |
. . . . . . 7
supp g
supp g supp
supp
|
81 | 80 | imbi2d 330 |
. . . . . 6
supp g
supp g supp
supp
|
82 | | mplcoe1.i |
. . . . . . . . 9
|
83 | | mplcoe1.r |
. . . . . . . . . 10
|
84 | | ringgrp 18552 |
. . . . . . . . . 10
|
85 | 83, 84 | syl 17 |
. . . . . . . . 9
|
86 | 1, 4, 17, 44, 82, 85 | mpl0 19441 |
. . . . . . . 8
|
87 | | fconstmpt 5163 |
. . . . . . . 8
|
88 | 86, 87 | syl6eq 2672 |
. . . . . . 7
|
89 | 88 | a1d 25 |
. . . . . 6
|
90 | | ssun1 3776 |
. . . . . . . . . . 11
|
91 | | sstr2 3610 |
. . . . . . . . . . 11
|
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . 10
|
93 | 92 | imim1i 63 |
. . . . . . . . 9
g g |
94 | | oveq1 6657 |
. . . . . . . . . . . 12
g
g |
95 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
96 | 1 | mplring 19452 |
. . . . . . . . . . . . . . . . 17
|
97 | 82, 83, 96 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
98 | | ringcmn 18581 |
. . . . . . . . . . . . . . . 16
CMnd |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . 15
CMnd |
100 | 99 | adantr 481 |
. . . . . . . . . . . . . 14
CMnd |
101 | | simprll 802 |
. . . . . . . . . . . . . 14
|
102 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
|
103 | 102 | unssad 3790 |
. . . . . . . . . . . . . . . 16
|
104 | 103 | sselda 3603 |
. . . . . . . . . . . . . . 15
|
105 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
106 | 83 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
107 | 1 | mpllmod 19451 |
. . . . . . . . . . . . . . . . . 18
|
108 | 105, 106,
107 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
109 | 6 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
|
110 | 1, 82, 83 | mplsca 19445 |
. . . . . . . . . . . . . . . . . . . 20
Scalar |
111 | 110 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Scalar |
112 | 111 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
Scalar |
113 | 109, 112 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . 17
Scalar |
114 | | mplcoe1.o |
. . . . . . . . . . . . . . . . . 18
|
115 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
116 | 1, 3, 17, 114, 4, 105, 106, 115 | mplmon 19463 |
. . . . . . . . . . . . . . . . 17
|
117 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
Scalar Scalar |
118 | | mplcoe1.n |
. . . . . . . . . . . . . . . . . 18
|
119 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
Scalar Scalar |
120 | 3, 117, 118, 119 | lmodvscl 18880 |
. . . . . . . . . . . . . . . . 17
Scalar
|
121 | 108, 113,
116, 120 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
122 | 121 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
123 | 104, 122 | syldan 487 |
. . . . . . . . . . . . . 14
|
124 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
125 | 124 | a1i 11 |
. . . . . . . . . . . . . 14
|
126 | | simprlr 803 |
. . . . . . . . . . . . . 14
|
127 | 82, 83, 107 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . 15
|
129 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
130 | 102 | unssbd 3791 |
. . . . . . . . . . . . . . . . . 18
|
131 | 124 | snss 4316 |
. . . . . . . . . . . . . . . . . 18
|
132 | 130, 131 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
133 | 129, 132 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
134 | 110 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Scalar |
135 | 134 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
Scalar |
136 | 133, 135 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
Scalar |
137 | 82 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
138 | 83 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
139 | 1, 3, 17, 114, 4, 137, 138, 132 | mplmon 19463 |
. . . . . . . . . . . . . . 15
|
140 | 3, 117, 118, 119 | lmodvscl 18880 |
. . . . . . . . . . . . . . 15
Scalar
|
141 | 128, 136,
139, 140 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
142 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
143 | | equequ2 1953 |
. . . . . . . . . . . . . . . . 17
|
144 | 143 | ifbid 4108 |
. . . . . . . . . . . . . . . 16
|
145 | 144 | mpteq2dv 4745 |
. . . . . . . . . . . . . . 15
|
146 | 142, 145 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
147 | 3, 95, 100, 101, 123, 125, 126, 141, 146 | gsumunsn 18359 |
. . . . . . . . . . . . 13
g g |
148 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
149 | 129 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
|
150 | 2, 17 | ring0cl 18569 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | 83, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
152 | 151 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
153 | 149, 152 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . 19
|
154 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
155 | 153, 154 | fmptd 6385 |
. . . . . . . . . . . . . . . . . 18
|
156 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
|
157 | 156, 15 | elmap 7886 |
. . . . . . . . . . . . . . . . . 18
|
158 | 155, 157 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
159 | 33, 2, 4, 34, 137 | psrbas 19378 |
. . . . . . . . . . . . . . . . 17
mPwSer
|
160 | 158, 159 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . 16
mPwSer |
161 | 15 | mptex 6486 |
. . . . . . . . . . . . . . . . . . 19
|
162 | | funmpt 5926 |
. . . . . . . . . . . . . . . . . . 19
|
163 | 161, 162,
19 | 3pm3.2i 1239 |
. . . . . . . . . . . . . . . . . 18
|
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
165 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . . 20
|
166 | 165 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
167 | 166 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . 18
|
168 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
169 | 167, 168 | suppss2 7329 |
. . . . . . . . . . . . . . . . 17
supp
|
170 | | suppssfifsupp 8290 |
. . . . . . . . . . . . . . . . 17
supp
finSupp |
171 | 164, 101,
169, 170 | syl12anc 1324 |
. . . . . . . . . . . . . . . 16
finSupp |
172 | 1, 33, 34, 17, 3 | mplelbas 19430 |
. . . . . . . . . . . . . . . 16
mPwSer finSupp |
173 | 160, 171,
172 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
174 | 1, 3, 148, 95, 173, 141 | mpladd 19442 |
. . . . . . . . . . . . . 14
|
175 | | ovexd 6680 |
. . . . . . . . . . . . . . 15
|
176 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
|
177 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
178 | 1, 118, 2, 3, 177, 4, 133, 139 | mplvsca 19447 |
. . . . . . . . . . . . . . . 16
|
179 | 133 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
180 | 2, 114 | ringidcl 18568 |
. . . . . . . . . . . . . . . . . . . 20
|
181 | 180, 150 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . 19
|
182 | 83, 181 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
183 | 182 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
184 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . 18
|
185 | 184 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
186 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
|
187 | 168, 179,
183, 185, 186 | offval2 6914 |
. . . . . . . . . . . . . . . 16
|
188 | 178, 187 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
189 | 168, 153,
175, 176, 188 | offval2 6914 |
. . . . . . . . . . . . . 14
|
190 | 138, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
191 | 2, 148, 17 | grplid 17452 |
. . . . . . . . . . . . . . . . . . . 20
|
192 | 190, 133,
191 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
193 | 192 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
194 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
195 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . . 20
|
196 | 194, 195 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
|
197 | 196 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
198 | 193, 197 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
|
199 | 126 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
200 | 196, 199 | eqneltrd 2720 |
. . . . . . . . . . . . . . . . . . 19
|
201 | 200 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . 18
|
202 | 196 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . 20
|
203 | 202 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
204 | 2, 177, 114 | ringridm 18572 |
. . . . . . . . . . . . . . . . . . . . 21
|
205 | 138, 133,
204 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
206 | 205 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
207 | 203, 206 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
208 | 201, 207 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
209 | | elun2 3781 |
. . . . . . . . . . . . . . . . . . 19
|
210 | 209 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
211 | 210 | iftrued 4094 |
. . . . . . . . . . . . . . . . 17
|
212 | 198, 208,
211 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . 16
|
213 | 85 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
214 | 2, 148, 17 | grprid 17453 |
. . . . . . . . . . . . . . . . . . 19
|
215 | 213, 153,
214 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
216 | 215 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
217 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
218 | 217, 195 | sylnib 318 |
. . . . . . . . . . . . . . . . . . . . 21
|
219 | 218 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . 20
|
220 | 219 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
221 | 2, 177, 17 | ringrz 18588 |
. . . . . . . . . . . . . . . . . . . . 21
|
222 | 138, 133,
221 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
223 | 222 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
224 | 220, 223 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
225 | 224 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
226 | | biorf 420 |
. . . . . . . . . . . . . . . . . . . 20
|
227 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . . 21
|
228 | | orcom 402 |
. . . . . . . . . . . . . . . . . . . . 21
|
229 | 227, 228 | bitri 264 |
. . . . . . . . . . . . . . . . . . . 20
|
230 | 226, 229 | syl6rbbr 279 |
. . . . . . . . . . . . . . . . . . 19
|
231 | 230 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
232 | 231 | ifbid 4108 |
. . . . . . . . . . . . . . . . 17
|
233 | 216, 225,
232 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . 16
|
234 | 212, 233 | pm2.61dan 832 |
. . . . . . . . . . . . . . 15
|
235 | 234 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
|
236 | 174, 189,
235 | 3eqtrrd 2661 |
. . . . . . . . . . . . 13
|
237 | 147, 236 | eqeq12d 2637 |
. . . . . . . . . . . 12
g g |
238 | 94, 237 | syl5ibr 236 |
. . . . . . . . . . 11
g
g |
239 | 238 | expr 643 |
. . . . . . . . . 10
g
g |
240 | 239 | a2d 29 |
. . . . . . . . 9
g g |
241 | 93, 240 | syl5 34 |
. . . . . . . 8
g g |
242 | 241 | expcom 451 |
. . . . . . 7
g g |
243 | 242 | a2d 29 |
. . . . . 6
g g |
244 | 54, 63, 72, 81, 89, 243 | findcard2s 8201 |
. . . . 5
supp
supp
g supp supp
|
245 | 38, 244 | mpcom 38 |
. . . 4
supp g supp
supp
|
246 | 32, 245 | mpd 15 |
. . 3
g supp
supp
|
247 | 28, 246 | eqtr4d 2659 |
. 2
g supp
|
248 | 32 | resmptd 5452 |
. . . 4
supp supp |
249 | 248 | oveq2d 6666 |
. . 3
g supp g supp
|
250 | | eqid 2622 |
. . . . 5
|
251 | 121, 250 | fmptd 6385 |
. . . 4
|
252 | 6, 13, 16, 20 | suppssr 7326 |
. . . . . . 7
supp |
253 | 252 | oveq1d 6665 |
. . . . . 6
supp |
254 | | eldifi 3732 |
. . . . . . 7
supp
|
255 | 111 | fveq2d 6195 |
. . . . . . . . . 10
Scalar |
256 | 17, 255 | syl5eq 2668 |
. . . . . . . . 9
Scalar |
257 | 256 | oveq1d 6665 |
. . . . . . . 8
Scalar
|
258 | | eqid 2622 |
. . . . . . . . . 10
Scalar Scalar |
259 | 3, 117, 118, 258, 44 | lmod0vs 18896 |
. . . . . . . . 9
Scalar |
260 | 108, 116,
259 | syl2anc 693 |
. . . . . . . 8
Scalar |
261 | 257, 260 | eqtrd 2656 |
. . . . . . 7
|
262 | 254, 261 | sylan2 491 |
. . . . . 6
supp |
263 | 253, 262 | eqtrd 2656 |
. . . . 5
supp |
264 | 263, 16 | suppss2 7329 |
. . . 4
supp supp |
265 | 15 | mptex 6486 |
. . . . . . 7
|
266 | | funmpt 5926 |
. . . . . . 7
|
267 | | fvex 6201 |
. . . . . . 7
|
268 | 265, 266,
267 | 3pm3.2i 1239 |
. . . . . 6
|
269 | 268 | a1i 11 |
. . . . 5
|
270 | | suppssfifsupp 8290 |
. . . . 5
supp supp supp finSupp |
271 | 269, 38, 264, 270 | syl12anc 1324 |
. . . 4
finSupp |
272 | 3, 44, 99, 16, 251, 264, 271 | gsumres 18314 |
. . 3
g supp g |
273 | 249, 272 | eqtr3d 2658 |
. 2
g supp
g |
274 | 247, 273 | eqtrd 2656 |
1
g |