Step | Hyp | Ref
| Expression |
1 | | frlmphl.v |
. . 3
|
2 | 1 | a1i 11 |
. 2
|
3 | | eqidd 2623 |
. 2
|
4 | | eqidd 2623 |
. 2
|
5 | | frlmphl.j |
. . 3
|
6 | 5 | a1i 11 |
. 2
|
7 | | frlmphl.o |
. . 3
|
8 | 7 | a1i 11 |
. 2
|
9 | | frlmphl.f |
. . . . 5
Field |
10 | | isfld 18756 |
. . . . 5
Field
|
11 | 9, 10 | sylib 208 |
. . . 4
|
12 | 11 | simpld 475 |
. . 3
|
13 | | frlmphl.i |
. . 3
|
14 | | frlmphl.y |
. . . 4
freeLMod
|
15 | 14 | frlmsca 20097 |
. . 3
Scalar |
16 | 12, 13, 15 | syl2anc 693 |
. 2
Scalar |
17 | | frlmphl.b |
. . 3
|
18 | 17 | a1i 11 |
. 2
|
19 | | eqidd 2623 |
. 2
|
20 | | frlmphl.t |
. . 3
|
21 | 20 | a1i 11 |
. 2
|
22 | | frlmphl.s |
. . 3
|
23 | 22 | a1i 11 |
. 2
|
24 | | frlmphl.0 |
. . 3
|
25 | 24 | a1i 11 |
. 2
|
26 | | drngring 18754 |
. . . . 5
|
27 | 12, 26 | syl 17 |
. . . 4
|
28 | 14 | frlmlmod 20093 |
. . . 4
|
29 | 27, 13, 28 | syl2anc 693 |
. . 3
|
30 | 16, 12 | eqeltrrd 2702 |
. . 3
Scalar |
31 | | eqid 2622 |
. . . 4
Scalar Scalar |
32 | 31 | islvec 19104 |
. . 3
Scalar |
33 | 29, 30, 32 | sylanbrc 698 |
. 2
|
34 | 11 | simprd 479 |
. . 3
|
35 | | frlmphl.u |
. . 3
|
36 | 17, 22, 34, 35 | idsrngd 18862 |
. 2
|
37 | 13 | 3ad2ant1 1082 |
. . . . 5
|
38 | 27 | 3ad2ant1 1082 |
. . . . 5
|
39 | | simp2 1062 |
. . . . 5
|
40 | | simp3 1063 |
. . . . 5
|
41 | 14, 17, 20, 1, 5 | frlmipval 20118 |
. . . . 5
g |
42 | 37, 38, 39, 40, 41 | syl22anc 1327 |
. . . 4
g |
43 | 14, 17, 1 | frlmbasmap 20103 |
. . . . . . . . 9
|
44 | 37, 39, 43 | syl2anc 693 |
. . . . . . . 8
|
45 | | elmapi 7879 |
. . . . . . . 8
|
46 | 44, 45 | syl 17 |
. . . . . . 7
|
47 | | ffn 6045 |
. . . . . . 7
|
48 | 46, 47 | syl 17 |
. . . . . 6
|
49 | 14, 17, 1 | frlmbasmap 20103 |
. . . . . . . . 9
|
50 | 37, 40, 49 | syl2anc 693 |
. . . . . . . 8
|
51 | | elmapi 7879 |
. . . . . . . 8
|
52 | 50, 51 | syl 17 |
. . . . . . 7
|
53 | | ffn 6045 |
. . . . . . 7
|
54 | 52, 53 | syl 17 |
. . . . . 6
|
55 | | inidm 3822 |
. . . . . 6
|
56 | | eqidd 2623 |
. . . . . 6
|
57 | | eqidd 2623 |
. . . . . 6
|
58 | 48, 54, 37, 37, 55, 56, 57 | offval 6904 |
. . . . 5
|
59 | 58 | oveq2d 6666 |
. . . 4
g g |
60 | 42, 59 | eqtrd 2656 |
. . 3
g |
61 | | ringcmn 18581 |
. . . . . 6
CMnd |
62 | 27, 61 | syl 17 |
. . . . 5
CMnd |
63 | 62 | 3ad2ant1 1082 |
. . . 4
CMnd |
64 | 38 | adantr 481 |
. . . . . 6
|
65 | 46 | ffvelrnda 6359 |
. . . . . 6
|
66 | 52 | ffvelrnda 6359 |
. . . . . 6
|
67 | 17, 20 | ringcl 18561 |
. . . . . 6
|
68 | 64, 65, 66, 67 | syl3anc 1326 |
. . . . 5
|
69 | | eqid 2622 |
. . . . 5
|
70 | 68, 69 | fmptd 6385 |
. . . 4
|
71 | | frlmphl.m |
. . . . 5
|
72 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 71, 35, 13 | frlmphllem 20119 |
. . . 4
finSupp |
73 | 17, 24, 63, 37, 70, 72 | gsumcl 18316 |
. . 3
g
|
74 | 60, 73 | eqeltrd 2701 |
. 2
|
75 | | eqid 2622 |
. . . 4
|
76 | 62 | 3ad2ant1 1082 |
. . . 4
CMnd |
77 | 13 | 3ad2ant1 1082 |
. . . 4
|
78 | 27 | 3ad2ant1 1082 |
. . . . . 6
|
79 | 78 | adantr 481 |
. . . . 5
|
80 | | simp2 1062 |
. . . . . 6
|
81 | 80 | adantr 481 |
. . . . 5
|
82 | | simp31 1097 |
. . . . . . . . 9
|
83 | 77, 82, 43 | syl2anc 693 |
. . . . . . . 8
|
84 | 83, 45 | syl 17 |
. . . . . . 7
|
85 | 84 | ffvelrnda 6359 |
. . . . . 6
|
86 | | simp33 1099 |
. . . . . . . . 9
|
87 | 14, 17, 1 | frlmbasmap 20103 |
. . . . . . . . 9
|
88 | 77, 86, 87 | syl2anc 693 |
. . . . . . . 8
|
89 | | elmapi 7879 |
. . . . . . . 8
|
90 | 88, 89 | syl 17 |
. . . . . . 7
|
91 | 90 | ffvelrnda 6359 |
. . . . . 6
|
92 | 17, 20 | ringcl 18561 |
. . . . . 6
|
93 | 79, 85, 91, 92 | syl3anc 1326 |
. . . . 5
|
94 | 17, 20 | ringcl 18561 |
. . . . 5
|
95 | 79, 81, 93, 94 | syl3anc 1326 |
. . . 4
|
96 | | simp32 1098 |
. . . . . . . 8
|
97 | 77, 96, 49 | syl2anc 693 |
. . . . . . 7
|
98 | 97, 51 | syl 17 |
. . . . . 6
|
99 | 98 | ffvelrnda 6359 |
. . . . 5
|
100 | 17, 20 | ringcl 18561 |
. . . . 5
|
101 | 79, 99, 91, 100 | syl3anc 1326 |
. . . 4
|
102 | | eqidd 2623 |
. . . 4
|
103 | | eqidd 2623 |
. . . 4
|
104 | | fveq2 6191 |
. . . . . . . . 9
|
105 | 104 | oveq2d 6666 |
. . . . . . . 8
|
106 | 105 | cbvmptv 4750 |
. . . . . . 7
|
107 | 106 | oveq1i 6660 |
. . . . . 6
|
108 | 17, 20 | ringcl 18561 |
. . . . . . . . . . . 12
|
109 | 79, 81, 85, 108 | syl3anc 1326 |
. . . . . . . . . . 11
|
110 | | eqid 2622 |
. . . . . . . . . . 11
|
111 | 109, 110 | fmptd 6385 |
. . . . . . . . . 10
|
112 | | ffn 6045 |
. . . . . . . . . 10
|
113 | 111, 112 | syl 17 |
. . . . . . . . 9
|
114 | 106 | fneq1i 5985 |
. . . . . . . . 9
|
115 | 113, 114 | sylib 208 |
. . . . . . . 8
|
116 | | ffn 6045 |
. . . . . . . . 9
|
117 | 90, 116 | syl 17 |
. . . . . . . 8
|
118 | | eqidd 2623 |
. . . . . . . . 9
|
119 | | simpr 477 |
. . . . . . . . . . 11
|
120 | 119 | fveq2d 6195 |
. . . . . . . . . 10
|
121 | 120 | oveq2d 6666 |
. . . . . . . . 9
|
122 | | simpr 477 |
. . . . . . . . 9
|
123 | | ovexd 6680 |
. . . . . . . . 9
|
124 | 118, 121,
122, 123 | fvmptd 6288 |
. . . . . . . 8
|
125 | | eqidd 2623 |
. . . . . . . 8
|
126 | 115, 117,
77, 77, 55, 124, 125 | offval 6904 |
. . . . . . 7
|
127 | 17, 20 | ringass 18564 |
. . . . . . . . 9
|
128 | 79, 81, 85, 91, 127 | syl13anc 1328 |
. . . . . . . 8
|
129 | 128 | mpteq2dva 4744 |
. . . . . . 7
|
130 | 126, 129 | eqtrd 2656 |
. . . . . 6
|
131 | 107, 130 | syl5eq 2668 |
. . . . 5
|
132 | | ovexd 6680 |
. . . . . 6
|
133 | | funmpt 5926 |
. . . . . . 7
|
134 | | eqidd 2623 |
. . . . . . . . 9
|
135 | | eqidd 2623 |
. . . . . . . . 9
|
136 | 113, 117,
77, 77, 55, 134, 135 | offval 6904 |
. . . . . . . 8
|
137 | 136 | funeqd 5910 |
. . . . . . 7
|
138 | 133, 137 | mpbiri 248 |
. . . . . 6
|
139 | | simp3 1063 |
. . . . . . . . 9
|
140 | 13, 139 | anim12i 590 |
. . . . . . . 8
|
141 | 140 | 3adant2 1080 |
. . . . . . 7
|
142 | 14, 24, 1 | frlmbasfsupp 20102 |
. . . . . . 7
finSupp
|
143 | 141, 142 | syl 17 |
. . . . . 6
finSupp |
144 | 17, 24 | ring0cl 18569 |
. . . . . . . 8
|
145 | 78, 144 | syl 17 |
. . . . . . 7
|
146 | 17, 20, 24 | ringrz 18588 |
. . . . . . . 8
|
147 | 78, 146 | sylan 488 |
. . . . . . 7
|
148 | 77, 145, 111, 90, 147 | suppofss2d 7333 |
. . . . . 6
supp
supp
|
149 | | fsuppsssupp 8291 |
. . . . . 6
finSupp supp
supp finSupp |
150 | 132, 138,
143, 148, 149 | syl22anc 1327 |
. . . . 5
finSupp |
151 | 131, 150 | eqbrtrrd 4677 |
. . . 4
finSupp
|
152 | | simp1 1061 |
. . . . 5
|
153 | | eleq1 2689 |
. . . . . . . . 9
|
154 | | id 22 |
. . . . . . . . . . 11
|
155 | 154, 154 | oveq12d 6668 |
. . . . . . . . . 10
|
156 | 155 | eqeq1d 2624 |
. . . . . . . . 9
|
157 | 153, 156 | 3anbi23d 1402 |
. . . . . . . 8
|
158 | | eqeq1 2626 |
. . . . . . . 8
|
159 | 157, 158 | imbi12d 334 |
. . . . . . 7
|
160 | 159, 71 | chvarv 2263 |
. . . . . 6
|
161 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 160, 35, 13 | frlmphllem 20119 |
. . . . 5
finSupp |
162 | 152, 96, 86, 161 | syl3anc 1326 |
. . . 4
finSupp
|
163 | 17, 24, 75, 76, 77, 95, 101, 102, 103, 151, 162 | gsummptfsadd 18324 |
. . 3
g g
g
|
164 | 14, 17, 20 | frlmip 20117 |
. . . . . . . . 9
g |
165 | 13, 12, 164 | syl2anc 693 |
. . . . . . . 8
g |
166 | 165, 5 | syl6reqr 2675 |
. . . . . . 7
g |
167 | | fveq1 6190 |
. . . . . . . . . . 11
|
168 | 167 | oveq1d 6665 |
. . . . . . . . . 10
|
169 | 168 | mpteq2dv 4745 |
. . . . . . . . 9
|
170 | 169 | oveq2d 6666 |
. . . . . . . 8
g g |
171 | | fveq1 6190 |
. . . . . . . . . . 11
|
172 | 171 | oveq2d 6666 |
. . . . . . . . . 10
|
173 | 172 | mpteq2dv 4745 |
. . . . . . . . 9
|
174 | 173 | oveq2d 6666 |
. . . . . . . 8
g g |
175 | 170, 174 | cbvmpt2v 6735 |
. . . . . . 7
g
g |
176 | 166, 175 | syl6eqr 2674 |
. . . . . 6
g
|
177 | 176 | 3ad2ant1 1082 |
. . . . 5
g |
178 | | simprl 794 |
. . . . . . . . 9
|
179 | 178 | fveq1d 6193 |
. . . . . . . 8
|
180 | | simprr 796 |
. . . . . . . . 9
|
181 | 180 | fveq1d 6193 |
. . . . . . . 8
|
182 | 179, 181 | oveq12d 6668 |
. . . . . . 7
|
183 | 182 | mpteq2dv 4745 |
. . . . . 6
|
184 | 183 | oveq2d 6666 |
. . . . 5
g g
|
185 | 29 | 3ad2ant1 1082 |
. . . . . . 7
|
186 | 16 | 3ad2ant1 1082 |
. . . . . . . . . . 11
Scalar |
187 | 186 | fveq2d 6195 |
. . . . . . . . . 10
Scalar |
188 | 17, 187 | syl5eq 2668 |
. . . . . . . . 9
Scalar |
189 | 80, 188 | eleqtrd 2703 |
. . . . . . . 8
Scalar |
190 | | eqid 2622 |
. . . . . . . . 9
|
191 | | eqid 2622 |
. . . . . . . . 9
Scalar Scalar |
192 | 1, 31, 190, 191 | lmodvscl 18880 |
. . . . . . . 8
Scalar
|
193 | 185, 189,
82, 192 | syl3anc 1326 |
. . . . . . 7
|
194 | | eqid 2622 |
. . . . . . . 8
|
195 | 1, 194 | lmodvacl 18877 |
. . . . . . 7
|
196 | 185, 193,
96, 195 | syl3anc 1326 |
. . . . . 6
|
197 | 14, 17, 1 | frlmbasmap 20103 |
. . . . . 6
|
198 | 77, 196, 197 | syl2anc 693 |
. . . . 5
|
199 | | ovexd 6680 |
. . . . 5
g |
200 | 177, 184,
198, 88, 199 | ovmpt2d 6788 |
. . . 4
g
|
201 | 14, 1, 78, 77, 193, 96, 75, 194 | frlmplusgval 20107 |
. . . . . . . . . 10
|
202 | 14, 17, 1 | frlmbasmap 20103 |
. . . . . . . . . . . . 13
|
203 | 77, 193, 202 | syl2anc 693 |
. . . . . . . . . . . 12
|
204 | | elmapi 7879 |
. . . . . . . . . . . 12
|
205 | | ffn 6045 |
. . . . . . . . . . . 12
|
206 | 203, 204,
205 | 3syl 18 |
. . . . . . . . . . 11
|
207 | 98, 53 | syl 17 |
. . . . . . . . . . 11
|
208 | 77 | adantr 481 |
. . . . . . . . . . . 12
|
209 | 82 | adantr 481 |
. . . . . . . . . . . 12
|
210 | 14, 1, 17, 208, 81, 209, 122, 190, 20 | frlmvscaval 20110 |
. . . . . . . . . . 11
|
211 | | eqidd 2623 |
. . . . . . . . . . 11
|
212 | 206, 207,
77, 77, 55, 210, 211 | offval 6904 |
. . . . . . . . . 10
|
213 | 201, 212 | eqtrd 2656 |
. . . . . . . . 9
|
214 | | ovexd 6680 |
. . . . . . . . 9
|
215 | 213, 214 | fvmpt2d 6293 |
. . . . . . . 8
|
216 | 215 | oveq1d 6665 |
. . . . . . 7
|
217 | 17, 75, 20 | ringdir 18567 |
. . . . . . . 8
|
218 | 79, 109, 99, 91, 217 | syl13anc 1328 |
. . . . . . 7
|
219 | 128 | oveq1d 6665 |
. . . . . . 7
|
220 | 216, 218,
219 | 3eqtrd 2660 |
. . . . . 6
|
221 | 220 | mpteq2dva 4744 |
. . . . 5
|
222 | 221 | oveq2d 6666 |
. . . 4
g g |
223 | 200, 222 | eqtrd 2656 |
. . 3
g
|
224 | | simprl 794 |
. . . . . . . . . . 11
|
225 | 224 | fveq1d 6193 |
. . . . . . . . . 10
|
226 | | simprr 796 |
. . . . . . . . . . 11
|
227 | 226 | fveq1d 6193 |
. . . . . . . . . 10
|
228 | 225, 227 | oveq12d 6668 |
. . . . . . . . 9
|
229 | 228 | mpteq2dv 4745 |
. . . . . . . 8
|
230 | 229 | oveq2d 6666 |
. . . . . . 7
g g
|
231 | | ovexd 6680 |
. . . . . . 7
g |
232 | 177, 230,
83, 88, 231 | ovmpt2d 6788 |
. . . . . 6
g
|
233 | 232 | oveq2d 6666 |
. . . . 5
g |
234 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 71, 35, 13 | frlmphllem 20119 |
. . . . . . 7
finSupp |
235 | 152, 82, 86, 234 | syl3anc 1326 |
. . . . . 6
finSupp
|
236 | 17, 24, 75, 20, 78, 77, 80, 93, 235 | gsummulc2 18607 |
. . . . 5
g
g
|
237 | 233, 236 | eqtr4d 2659 |
. . . 4
g
|
238 | | simprl 794 |
. . . . . . . . 9
|
239 | 238 | fveq1d 6193 |
. . . . . . . 8
|
240 | | simprr 796 |
. . . . . . . . 9
|
241 | 240 | fveq1d 6193 |
. . . . . . . 8
|
242 | 239, 241 | oveq12d 6668 |
. . . . . . 7
|
243 | 242 | mpteq2dv 4745 |
. . . . . 6
|
244 | 243 | oveq2d 6666 |
. . . . 5
g g
|
245 | | ovexd 6680 |
. . . . 5
g |
246 | 177, 244,
97, 88, 245 | ovmpt2d 6788 |
. . . 4
g
|
247 | 237, 246 | oveq12d 6668 |
. . 3
g
g
|
248 | 163, 223,
247 | 3eqtr4d 2666 |
. 2
|
249 | 34 | 3ad2ant1 1082 |
. . . . . . 7
|
250 | 249 | adantr 481 |
. . . . . 6
|
251 | 17, 20 | crngcom 18562 |
. . . . . 6
|
252 | 250, 66, 65, 251 | syl3anc 1326 |
. . . . 5
|
253 | 252 | mpteq2dva 4744 |
. . . 4
|
254 | 253 | oveq2d 6666 |
. . 3
g
g
|
255 | 176 | 3ad2ant1 1082 |
. . . 4
g |
256 | | simprl 794 |
. . . . . . . 8
|
257 | 256 | fveq1d 6193 |
. . . . . . 7
|
258 | | simprr 796 |
. . . . . . . 8
|
259 | 258 | fveq1d 6193 |
. . . . . . 7
|
260 | 257, 259 | oveq12d 6668 |
. . . . . 6
|
261 | 260 | mpteq2dv 4745 |
. . . . 5
|
262 | 261 | oveq2d 6666 |
. . . 4
g
g
|
263 | | ovexd 6680 |
. . . 4
g
|
264 | 255, 262,
50, 44, 263 | ovmpt2d 6788 |
. . 3
g |
265 | 35 | ralrimiva 2966 |
. . . . . 6
|
266 | 265 | 3ad2ant1 1082 |
. . . . 5
|
267 | | fveq2 6191 |
. . . . . . 7
|
268 | | id 22 |
. . . . . . 7
|
269 | 267, 268 | eqeq12d 2637 |
. . . . . 6
|
270 | 269 | rspcv 3305 |
. . . . 5
|
271 | 74, 266, 270 | sylc 65 |
. . . 4
|
272 | 271, 60 | eqtrd 2656 |
. . 3
g |
273 | 254, 264,
272 | 3eqtr4rd 2667 |
. 2
|
274 | 2, 3, 4, 6, 8, 16,
18, 19, 21, 23, 25, 33, 36, 74, 248, 71, 273 | isphld 19999 |
1
|