Step | Hyp | Ref
| Expression |
1 | | frlmphl.v |
. . 3
     |
2 | 1 | a1i 11 |
. 2
       |
3 | | eqidd 2452 |
. 2
         |
4 | | eqidd 2452 |
. 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 17984 |
. . . . 5
 Field 
   |
11 | 9, 10 | sylib 200 |
. . . 4
 
   |
12 | 11 | simpld 461 |
. . 3
   |
13 | | frlmphl.i |
. . 3
   |
14 | | frlmphl.y |
. . . 4
 freeLMod
  |
15 | 14 | frlmsca 19316 |
. . 3
   Scalar    |
16 | 12, 13, 15 | syl2anc 667 |
. 2
 Scalar    |
17 | | frlmphl.b |
. . 3
     |
18 | 17 | a1i 11 |
. 2
       |
19 | | eqidd 2452 |
. 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 17982 |
. . . . 5
   |
27 | 12, 26 | syl 17 |
. . . 4
   |
28 | 14 | frlmlmod 19312 |
. . . 4
     |
29 | 27, 13, 28 | syl2anc 667 |
. . 3
   |
30 | 16, 12 | eqeltrrd 2530 |
. . 3
 Scalar    |
31 | | eqid 2451 |
. . . 4
Scalar  Scalar   |
32 | 31 | islvec 18327 |
. . 3

 Scalar     |
33 | 29, 30, 32 | sylanbrc 670 |
. 2
   |
34 | 11 | simprd 465 |
. . 3
   |
35 | | frlmphl.u |
. . 3
 
     |
36 | 17, 22, 34, 35 | idsrngd 18090 |
. 2
   |
37 | 13 | 3ad2ant1 1029 |
. . . . 5
 

  |
38 | 27 | 3ad2ant1 1029 |
. . . . 5
 

  |
39 | | simp2 1009 |
. . . . 5
 

  |
40 | | simp3 1010 |
. . . . 5
 

  |
41 | 14, 17, 20, 1, 5 | frlmipval 19337 |
. . . . 5
  
       g       |
42 | 37, 38, 39, 40, 41 | syl22anc 1269 |
. . . 4
 

   g       |
43 | 14, 17, 1 | frlmbasmap 19322 |
. . . . . . . . 9
 
     |
44 | 37, 39, 43 | syl2anc 667 |
. . . . . . . 8
 


   |
45 | | elmapi 7493 |
. . . . . . . 8
         |
46 | 44, 45 | syl 17 |
. . . . . . 7
 

      |
47 | | ffn 5728 |
. . . . . . 7
       |
48 | 46, 47 | syl 17 |
. . . . . 6
 

  |
49 | 14, 17, 1 | frlmbasmap 19322 |
. . . . . . . . 9
 
     |
50 | 37, 40, 49 | syl2anc 667 |
. . . . . . . 8
 


   |
51 | | elmapi 7493 |
. . . . . . . 8
         |
52 | 50, 51 | syl 17 |
. . . . . . 7
 

      |
53 | | ffn 5728 |
. . . . . . 7
    
  |
54 | 52, 53 | syl 17 |
. . . . . 6
 

  |
55 | | inidm 3641 |
. . . . . 6
   |
56 | | eqidd 2452 |
. . . . . 6
  
            |
57 | | eqidd 2452 |
. . . . . 6
  
            |
58 | 48, 54, 37, 37, 55, 56, 57 | offval 6538 |
. . . . 5
 

 
               |
59 | 58 | oveq2d 6306 |
. . . 4
 

 g      g                |
60 | 42, 59 | eqtrd 2485 |
. . 3
 

   g                |
61 | | ringcmn 17811 |
. . . . . 6

CMnd |
62 | 27, 61 | syl 17 |
. . . . 5
 CMnd |
63 | 62 | 3ad2ant1 1029 |
. . . 4
 

CMnd |
64 | 38 | adantr 467 |
. . . . . 6
  
    |
65 | 46 | ffvelrnda 6022 |
. . . . . 6
  
        |
66 | 52 | ffvelrnda 6022 |
. . . . . 6
  
        |
67 | 17, 20 | ringcl 17794 |
. . . . . 6
     
         
       |
68 | 64, 65, 66, 67 | syl3anc 1268 |
. . . . 5
  
      
       |
69 | | eqid 2451 |
. . . . 5
                         |
70 | 68, 69 | fmptd 6046 |
. . . 4
 


                 |
71 | | frlmphl.m |
. . . . 5
 
 
  |
72 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 71, 35, 13 | frlmphllem 19338 |
. . . 4
 


           finSupp  |
73 | 17, 24, 63, 37, 70, 72 | gsumcl 17549 |
. . 3
 

 g      
         |
74 | 60, 73 | eqeltrd 2529 |
. 2
 

    |
75 | | eqid 2451 |
. . . 4
       |
76 | 62 | 3ad2ant1 1029 |
. . . 4
 
  
CMnd |
77 | 13 | 3ad2ant1 1029 |
. . . 4
 
  
  |
78 | 27 | 3ad2ant1 1029 |
. . . . . 6
 
  
  |
79 | 78 | adantr 467 |
. . . . 5
  

 
   |
80 | | simp2 1009 |
. . . . . 6
 
     |
81 | 80 | adantr 467 |
. . . . 5
  

 
   |
82 | | simp31 1044 |
. . . . . . . . 9
 
     |
83 | 77, 82, 43 | syl2anc 667 |
. . . . . . . 8
 
       |
84 | 83, 45 | syl 17 |
. . . . . . 7
 
         |
85 | 84 | ffvelrnda 6022 |
. . . . . 6
  

 
       |
86 | | simp33 1046 |
. . . . . . . . 9
 
     |
87 | 14, 17, 1 | frlmbasmap 19322 |
. . . . . . . . 9
 
     |
88 | 77, 86, 87 | syl2anc 667 |
. . . . . . . 8
 
       |
89 | | elmapi 7493 |
. . . . . . . 8
         |
90 | 88, 89 | syl 17 |
. . . . . . 7
 
         |
91 | 90 | ffvelrnda 6022 |
. . . . . 6
  

 
       |
92 | 17, 20 | ringcl 17794 |
. . . . . 6
     
         
       |
93 | 79, 85, 91, 92 | syl3anc 1268 |
. . . . 5
  

 
     
       |
94 | 17, 20 | ringcl 17794 |
. . . . 5
 
    
      
             |
95 | 79, 81, 93, 94 | syl3anc 1268 |
. . . 4
  

 
 
             |
96 | | simp32 1045 |
. . . . . . . 8
 
  
  |
97 | 77, 96, 49 | syl2anc 667 |
. . . . . . 7
 
  
    |
98 | 97, 51 | syl 17 |
. . . . . 6
 
         |
99 | 98 | ffvelrnda 6022 |
. . . . 5
  

 
       |
100 | 17, 20 | ringcl 17794 |
. . . . 5
     
         
       |
101 | 79, 99, 91, 100 | syl3anc 1268 |
. . . 4
  

 
     
       |
102 | | eqidd 2452 |
. . . 4
 
         
                       |
103 | | eqidd 2452 |
. . . 4
 
                    
        |
104 | | fveq2 5865 |
. . . . . . . . 9
           |
105 | 104 | oveq2d 6306 |
. . . . . . . 8
 
             |
106 | 105 | cbvmptv 4495 |
. . . . . . 7
                 |
107 | 106 | oveq1i 6300 |
. . . . . 6
                       |
108 | 17, 20 | ringcl 17794 |
. . . . . . . . . . . 12
 
     
       |
109 | 79, 81, 85, 108 | syl3anc 1268 |
. . . . . . . . . . 11
  

 
 
       |
110 | | eqid 2451 |
. . . . . . . . . . 11
                 |
111 | 109, 110 | fmptd 6046 |
. . . . . . . . . 10
 
                 |
112 | | ffn 5728 |
. . . . . . . . . 10
                       |
113 | 111, 112 | syl 17 |
. . . . . . . . 9
 
             |
114 | 106 | fneq1i 5670 |
. . . . . . . . 9
        

         |
115 | 113, 114 | sylib 200 |
. . . . . . . 8
 
             |
116 | | ffn 5728 |
. . . . . . . . 9
       |
117 | 90, 116 | syl 17 |
. . . . . . . 8
 
     |
118 | | eqidd 2452 |
. . . . . . . . 9
  

 
                   |
119 | | simpr 463 |
. . . . . . . . . . 11
   

      |
120 | 119 | fveq2d 5869 |
. . . . . . . . . 10
   

              |
121 | 120 | oveq2d 6306 |
. . . . . . . . 9
   

    
             |
122 | | simpr 463 |
. . . . . . . . 9
  

 
   |
123 | | ovex 6318 |
. . . . . . . . . 10
       |
124 | 123 | a1i 11 |
. . . . . . . . 9
  

 
 
       |
125 | 118, 121,
122, 124 | fvmptd 5954 |
. . . . . . . 8
  

 
                     |
126 | | eqidd 2452 |
. . . . . . . 8
  

 
           |
127 | 115, 117,
77, 77, 55, 125, 126 | offval 6538 |
. . . . . . 7
 
                              |
128 | 17, 20 | ringass 17797 |
. . . . . . . . 9
            
 
                        |
129 | 79, 81, 85, 91, 128 | syl13anc 1270 |
. . . . . . . 8
  

 
       
          
        |
130 | 129 | mpteq2dva 4489 |
. . . . . . 7
 
                                 |
131 | 127, 130 | eqtrd 2485 |
. . . . . 6
 
                              |
132 | 107, 131 | syl5eq 2497 |
. . . . 5
 
                              |
133 | | ovex 6318 |
. . . . . . 7
            |
134 | 133 | a1i 11 |
. . . . . 6
 
                |
135 | | funmpt 5618 |
. . . . . . 7
                     |
136 | | eqidd 2452 |
. . . . . . . . 9
  

 
                           |
137 | | eqidd 2452 |
. . . . . . . . 9
  

 
           |
138 | 113, 117,
77, 77, 55, 136, 137 | offval 6538 |
. . . . . . . 8
 
                                    |
139 | 138 | funeqd 5603 |
. . . . . . 7
 
   
          
             
         |
140 | 135, 139 | mpbiri 237 |
. . . . . 6
 
                |
141 | | simp3 1010 |
. . . . . . . . 9
 
   |
142 | 13, 141 | anim12i 570 |
. . . . . . . 8
 

  
   |
143 | 142 | 3adant2 1027 |
. . . . . . 7
 
   
   |
144 | 14, 24, 1 | frlmbasfsupp 19321 |
. . . . . . 7
 
 finSupp
 |
145 | 143, 144 | syl 17 |
. . . . . 6
 
   finSupp  |
146 | 17, 24 | ring0cl 17802 |
. . . . . . . 8

  |
147 | 78, 146 | syl 17 |
. . . . . . 7
 
     |
148 | 17, 20, 24 | ringrz 17818 |
. . . . . . . 8
   
 |
149 | 78, 148 | sylan 474 |
. . . . . . 7
  

 
 
 |
150 | 77, 147, 111, 90, 149 | suppofss2d 6953 |
. . . . . 6
 
               supp
 supp
  |
151 | | fsuppsssupp 7899 |
. . . . . 6
                           finSupp             supp
 supp              finSupp  |
152 | 134, 140,
145, 150, 151 | syl22anc 1269 |
. . . . 5
 
              finSupp  |
153 | 132, 152 | eqbrtrrd 4425 |
. . . 4
 
         
       finSupp
 |
154 | | simp1 1008 |
. . . . 5
 
     |
155 | | eleq1 2517 |
. . . . . . . . 9
 
   |
156 | | id 22 |
. . . . . . . . . . 11
   |
157 | 156, 156 | oveq12d 6308 |
. . . . . . . . . 10
 
     |
158 | 157 | eqeq1d 2453 |
. . . . . . . . 9
   
    |
159 | 155, 158 | 3anbi23d 1342 |
. . . . . . . 8
  


 
    |
160 | | eqeq1 2455 |
. . . . . . . 8
 
   |
161 | 159, 160 | imbi12d 322 |
. . . . . . 7
   
    


    |
162 | 161, 71 | chvarv 2107 |
. . . . . 6
 
 
  |
163 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 162, 35, 13 | frlmphllem 19338 |
. . . . 5
 


           finSupp  |
164 | 154, 96, 86, 163 | syl3anc 1268 |
. . . 4
 
               finSupp
 |
165 | 17, 24, 75, 76, 77, 95, 101, 102, 103, 153, 164 | gsummptfsadd 17557 |
. . 3
 
    g                                   g       
              g 
               |
166 | 14, 17, 20 | frlmip 19336 |
. . . . . . . . 9
 
        g                     |
167 | 13, 12, 166 | syl2anc 667 |
. . . . . . . 8
        g                     |
168 | 167, 5 | syl6reqr 2504 |
. . . . . . 7
        g                 |
169 | | fveq1 5864 |
. . . . . . . . . . 11
           |
170 | 169 | oveq1d 6305 |
. . . . . . . . . 10
     
                 |
171 | 170 | mpteq2dv 4490 |
. . . . . . . . 9
      
                    |
172 | 171 | oveq2d 6306 |
. . . . . . . 8
  g               g                |
173 | | fveq1 5864 |
. . . . . . . . . . 11
           |
174 | 173 | oveq2d 6306 |
. . . . . . . . . 10
     
                 |
175 | 174 | mpteq2dv 4490 |
. . . . . . . . 9
      
                    |
176 | 175 | oveq2d 6306 |
. . . . . . . 8
  g               g                |
177 | 172, 176 | cbvmpt2v 6371 |
. . . . . . 7
       g 
                    g                |
178 | 168, 177 | syl6eqr 2503 |
. . . . . 6
        g 
               |
179 | 178 | 3ad2ant1 1029 |
. . . . 5
 
  
       g                 |
180 | | simprl 764 |
. . . . . . . . 9
  

 
                                   |
181 | 180 | fveq1d 5867 |
. . . . . . . 8
  

 
                                           |
182 | | simprr 766 |
. . . . . . . . 9
  

 
                    |
183 | 182 | fveq1d 5867 |
. . . . . . . 8
  

 
                            |
184 | 181, 183 | oveq12d 6308 |
. . . . . . 7
  

 
                                               
       |
185 | 184 | mpteq2dv 4490 |
. . . . . 6
  

 
                                                           |
186 | 185 | oveq2d 6306 |
. . . . 5
  

 
                   g               g 
                             |
187 | 29 | 3ad2ant1 1029 |
. . . . . . 7
 
  
  |
188 | 16 | 3ad2ant1 1029 |
. . . . . . . . . . 11
 
  
Scalar    |
189 | 188 | fveq2d 5869 |
. . . . . . . . . 10
 
          Scalar     |
190 | 17, 189 | syl5eq 2497 |
. . . . . . . . 9
 
  
   Scalar     |
191 | 80, 190 | eleqtrd 2531 |
. . . . . . . 8
 
      Scalar     |
192 | | eqid 2451 |
. . . . . . . . 9
         |
193 | | eqid 2451 |
. . . . . . . . 9
   Scalar      Scalar    |
194 | 1, 31, 192, 193 | lmodvscl 18108 |
. . . . . . . 8
     Scalar  
           |
195 | 187, 191,
82, 194 | syl3anc 1268 |
. . . . . . 7
 
             |
196 | | eqid 2451 |
. . . . . . . 8
       |
197 | 1, 196 | lmodvacl 18105 |
. . . . . . 7
                            |
198 | 187, 195,
96, 197 | syl3anc 1268 |
. . . . . 6
 
                    |
199 | 14, 17, 1 | frlmbasmap 19322 |
. . . . . 6
                                     |
200 | 77, 198, 199 | syl2anc 667 |
. . . . 5
 
                      |
201 | | ovex 6318 |
. . . . . 6
 g 
                            |
202 | 201 | a1i 11 |
. . . . 5
 
    g                               |
203 | 179, 186,
200, 88, 202 | ovmpt2d 6424 |
. . . 4
 
                     g 
                             |
204 | 14, 1, 78, 77, 195, 96, 75, 196 | frlmplusgval 19326 |
. . . . . . . . . 10
 
                                    |
205 | 14, 17, 1 | frlmbasmap 19322 |
. . . . . . . . . . . . 13
                       |
206 | 77, 195, 205 | syl2anc 667 |
. . . . . . . . . . . 12
 
               |
207 | | elmapi 7493 |
. . . . . . . . . . . 12
                         |
208 | | ffn 5728 |
. . . . . . . . . . . 12
                       |
209 | 206, 207,
208 | 3syl 18 |
. . . . . . . . . . 11
 
             |
210 | 98, 53 | syl 17 |
. . . . . . . . . . 11
 
  
  |
211 | 77 | adantr 467 |
. . . . . . . . . . . 12
  

 
   |
212 | 82 | adantr 467 |
. . . . . . . . . . . 12
  

 
   |
213 | 14, 1, 17, 211, 81, 212, 122, 192, 20 | frlmvscaval 19329 |
. . . . . . . . . . 11
  

 
                     |
214 | | eqidd 2452 |
. . . . . . . . . . 11
  

 
           |
215 | 209, 210,
77, 77, 55, 213, 214 | offval 6538 |
. . . . . . . . . 10
 
                                        |
216 | 204, 215 | eqtrd 2485 |
. . . . . . . . 9
 
                                       |
217 | | ovex 6318 |
. . . . . . . . . 10
                  |
218 | 217 | a1i 11 |
. . . . . . . . 9
  

 
                    |
219 | 216, 218 | fvmpt2d 5959 |
. . . . . . . 8
  

 
                                       |
220 | 219 | oveq1d 6305 |
. . . . . . 7
  

 
                    
                              |
221 | 17, 75, 20 | ringdir 17800 |
. . . . . . . 8
                  
                                                      |
222 | 79, 109, 99, 91, 221 | syl13anc 1270 |
. . . . . . 7
  

 
                                                       |
223 | 129 | oveq1d 6305 |
. . . . . . 7
  

 
                                                             |
224 | 220, 222,
223 | 3eqtrd 2489 |
. . . . . 6
  

 
                    
                                    |
225 | 224 | mpteq2dva 4489 |
. . . . 5
 
                                     
                         |
226 | 225 | oveq2d 6306 |
. . . 4
 
    g                              g                                   |
227 | 203, 226 | eqtrd 2485 |
. . 3
 
                     g 
                                 |
228 | | simprl 764 |
. . . . . . . . . . 11
  

 

    |
229 | 228 | fveq1d 5867 |
. . . . . . . . . 10
  

 

            |
230 | | simprr 766 |
. . . . . . . . . . 11
  

 

    |
231 | 230 | fveq1d 5867 |
. . . . . . . . . 10
  

 

            |
232 | 229, 231 | oveq12d 6308 |
. . . . . . . . 9
  

 

                
       |
233 | 232 | mpteq2dv 4490 |
. . . . . . . 8
  

 

                            |
234 | 233 | oveq2d 6306 |
. . . . . . 7
  

 

   g               g 
              |
235 | | ovex 6318 |
. . . . . . . 8
 g 
             |
236 | 235 | a1i 11 |
. . . . . . 7
 
    g                |
237 | 179, 234,
83, 88, 236 | ovmpt2d 6424 |
. . . . . 6
 
      g 
              |
238 | 237 | oveq2d 6306 |
. . . . 5
 
    
    g                 |
239 | 14, 17, 20, 1, 5, 7,
24, 22, 9, 71, 35, 13 | frlmphllem 19338 |
. . . . . . 7
 


           finSupp  |
240 | 154, 82, 86, 239 | syl3anc 1268 |
. . . . . 6
 
               finSupp
 |
241 | 17, 24, 75, 20, 78, 77, 80, 93, 240 | gsummulc2 17835 |
. . . . 5
 
    g       
          g 
               |
242 | 238, 241 | eqtr4d 2488 |
. . . 4
 
    
   g 
     
          |
243 | | simprl 764 |
. . . . . . . . 9
  

 

    |
244 | 243 | fveq1d 5867 |
. . . . . . . 8
  

 

            |
245 | | simprr 766 |
. . . . . . . . 9
  

 

    |
246 | 245 | fveq1d 5867 |
. . . . . . . 8
  

 

            |
247 | 244, 246 | oveq12d 6308 |
. . . . . . 7
  

 

                
       |
248 | 247 | mpteq2dv 4490 |
. . . . . 6
  

 

                            |
249 | 248 | oveq2d 6306 |
. . . . 5
  

 

   g               g 
              |
250 | | ovex 6318 |
. . . . . 6
 g 
             |
251 | 250 | a1i 11 |
. . . . 5
 
    g                |
252 | 179, 249,
97, 88, 251 | ovmpt2d 6424 |
. . . 4
 
      g 
              |
253 | 242, 252 | oveq12d 6308 |
. . 3
 
                  g 
     
              g 
               |
254 | 165, 227,
253 | 3eqtr4d 2495 |
. 2
 
                                   |
255 | 34 | 3ad2ant1 1029 |
. . . . . . 7
 

  |
256 | 255 | adantr 467 |
. . . . . 6
  
    |
257 | 17, 20 | crngcom 17795 |
. . . . . 6
     
         
                 |
258 | 256, 66, 65, 257 | syl3anc 1268 |
. . . . 5
  
      
                 |
259 | 258 | mpteq2dva 4489 |
. . . 4
 


                         |
260 | 259 | oveq2d 6306 |
. . 3
 

 g      
        g 
              |
261 | 178 | 3ad2ant1 1029 |
. . . 4
 

       g                 |
262 | | simprl 764 |
. . . . . . . 8
  
 
 
  |
263 | 262 | fveq1d 5867 |
. . . . . . 7
  
 
 
          |
264 | | simprr 766 |
. . . . . . . 8
  
 
 
  |
265 | 264 | fveq1d 5867 |
. . . . . . 7
  
 
 
          |
266 | 263, 265 | oveq12d 6308 |
. . . . . 6
  
 
 
              
       |
267 | 266 | mpteq2dv 4490 |
. . . . 5
  
 
 

                         |
268 | 267 | oveq2d 6306 |
. . . 4
  
 
 
 g      
        g 
              |
269 | | ovex 6318 |
. . . . 5
 g 
             |
270 | 269 | a1i 11 |
. . . 4
 

 g      
         |
271 | 261, 268,
50, 44, 270 | ovmpt2d 6424 |
. . 3
 

   g                |
272 | 35 | ralrimiva 2802 |
. . . . . 6
      |
273 | 272 | 3ad2ant1 1029 |
. . . . 5
 


    |
274 | | fveq2 5865 |
. . . . . . 7
      
    |
275 | | id 22 |
. . . . . . 7
       |
276 | 274, 275 | eqeq12d 2466 |
. . . . . 6
     
         |
277 | 276 | rspcv 3146 |
. . . . 5
    
           |
278 | 74, 273, 277 | sylc 62 |
. . . 4
 

        |
279 | 278, 60 | eqtrd 2485 |
. . 3
 

     g                |
280 | 260, 271,
279 | 3eqtr4rd 2496 |
. 2
 

        |
281 | 2, 3, 4, 6, 8, 16,
18, 19, 21, 23, 25, 33, 36, 74, 254, 71, 280 | isphld 19221 |
1
   |