Step | Hyp | Ref
| Expression |
1 | | mplcoe1.p |
. . . . . 6
 mPoly   |
2 | | eqid 2471 |
. . . . . 6
         |
3 | | mplcoe1.b |
. . . . . 6
     |
4 | | mplcoe1.d |
. . . . . 6
          |
5 | | mplcoe1.x |
. . . . . 6
   |
6 | 1, 2, 3, 4, 5 | mplelf 18734 |
. . . . 5
           |
7 | 6 | feqmptd 5932 |
. . . 4
         |
8 | | iftrue 3878 |
. . . . . . 7
  supp    supp 
    
      |
9 | 8 | adantl 473 |
. . . . . 6
     supp 
   supp             |
10 | | eldif 3400 |
. . . . . . . 8
   supp
   supp    |
11 | | ifid 3909 |
. . . . . . . . 9
   supp                 |
12 | | ssid 3437 |
. . . . . . . . . . . 12
 supp  supp  |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
  supp  supp   |
14 | | ovex 6336 |
. . . . . . . . . . . . 13
   |
15 | 4, 14 | rabex2 4552 |
. . . . . . . . . . . 12
 |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
   |
17 | | mplcoe1.z |
. . . . . . . . . . . . 13
     |
18 | | fvex 5889 |
. . . . . . . . . . . . 13
     |
19 | 17, 18 | eqeltri 2545 |
. . . . . . . . . . . 12
 |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
   |
21 | 6, 13, 16, 20 | suppssr 6965 |
. . . . . . . . . 10
 

 supp        |
22 | 21 | ifeq2d 3891 |
. . . . . . . . 9
 

 supp      supp 
             supp         |
23 | 11, 22 | syl5reqr 2520 |
. . . . . . . 8
 

 supp      supp 
    
      |
24 | 10, 23 | sylan2br 484 |
. . . . . . 7
 

 supp      supp
            |
25 | 24 | anassrs 660 |
. . . . . 6
   
 supp     supp
            |
26 | 9, 25 | pm2.61dan 808 |
. . . . 5
 
    supp
            |
27 | 26 | mpteq2dva 4482 |
. . . 4
     supp                |
28 | 7, 27 | eqtr4d 2508 |
. . 3
     supp          |
29 | | suppssdm 6946 |
. . . . 5
 supp  |
30 | | fdm 5745 |
. . . . . 6
           |
31 | 6, 30 | syl 17 |
. . . . 5
   |
32 | 29, 31 | syl5sseq 3466 |
. . . 4
  supp   |
33 | | eqid 2471 |
. . . . . . . . 9
 mPwSer   mPwSer   |
34 | | eqid 2471 |
. . . . . . . . 9
    mPwSer       mPwSer    |
35 | 1, 33, 34, 17, 3 | mplelbas 18731 |
. . . . . . . 8

     mPwSer   finSupp   |
36 | 35 | simprbi 471 |
. . . . . . 7
 finSupp  |
37 | 5, 36 | syl 17 |
. . . . . 6
 finSupp
 |
38 | 37 | fsuppimpd 7908 |
. . . . 5
  supp   |
39 | | sseq1 3439 |
. . . . . . . 8


   |
40 | | mpteq1 4476 |
. . . . . . . . . . . 12

                            |
41 | | mpt0 5715 |
. . . . . . . . . . . 12
              |
42 | 40, 41 | syl6eq 2521 |
. . . . . . . . . . 11

               |
43 | 42 | oveq2d 6324 |
. . . . . . . . . 10

 g                g    |
44 | | eqid 2471 |
. . . . . . . . . . 11
         |
45 | 44 | gsum0 16599 |
. . . . . . . . . 10
 g       |
46 | 43, 45 | syl6eq 2521 |
. . . . . . . . 9

 g                     |
47 | | noel 3726 |
. . . . . . . . . . . 12
 |
48 | | eleq2 2538 |
. . . . . . . . . . . 12


   |
49 | 47, 48 | mtbiri 310 |
. . . . . . . . . . 11

  |
50 | 49 | iffalsed 3883 |
. . . . . . . . . 10

         |
51 | 50 | mpteq2dv 4483 |
. . . . . . . . 9

             |
52 | 46, 51 | eqeq12d 2486 |
. . . . . . . 8

  g                                 |
53 | 39, 52 | imbi12d 327 |
. . . . . . 7

 
 g                         
          |
54 | 53 | imbi2d 323 |
. . . . . 6

    g                           

          |
55 | | sseq1 3439 |
. . . . . . . 8
 
   |
56 | | mpteq1 4476 |
. . . . . . . . . 10
      

                     |
57 | 56 | oveq2d 6324 |
. . . . . . . . 9
  g                g                 |
58 | | eleq2 2538 |
. . . . . . . . . . 11
 
   |
59 | 58 | ifbid 3894 |
. . . . . . . . . 10
        
          |
60 | 59 | mpteq2dv 4483 |
. . . . . . . . 9
                       |
61 | 57, 60 | eqeq12d 2486 |
. . . . . . . 8
   g                          g                            |
62 | 55, 61 | imbi12d 327 |
. . . . . . 7
    g                         

 g      

                     |
63 | 62 | imbi2d 323 |
. . . . . 6
  
  g                          
   g                              |
64 | | sseq1 3439 |
. . . . . . . 8
             |
65 | | mpteq1 4476 |
. . . . . . . . . 10
                           

        |
66 | 65 | oveq2d 6324 |
. . . . . . . . 9
      g                g                     |
67 | | eleq2 2538 |
. . . . . . . . . . 11
             |
68 | 67 | ifbid 3894 |
. . . . . . . . . 10
                           |
69 | 68 | mpteq2dv 4483 |
. . . . . . . . 9
                               |
70 | 66, 69 | eqeq12d 2486 |
. . . . . . . 8
       g                          g                                    |
71 | 64, 70 | imbi12d 327 |
. . . . . . 7
        g                         
      g                                     |
72 | 71 | imbi2d 323 |
. . . . . 6
         g                          
       g                                      |
73 | | sseq1 3439 |
. . . . . . . 8
  supp   supp    |
74 | | mpteq1 4476 |
. . . . . . . . . 10
  supp                supp               |
75 | 74 | oveq2d 6324 |
. . . . . . . . 9
  supp  g                g   supp
    

         |
76 | | eleq2 2538 |
. . . . . . . . . . 11
  supp   supp
   |
77 | 76 | ifbid 3894 |
. . . . . . . . . 10
  supp            supp         |
78 | 77 | mpteq2dv 4483 |
. . . . . . . . 9
  supp               supp 
        |
79 | 75, 78 | eqeq12d 2486 |
. . . . . . . 8
  supp   g                          g   supp                  supp           |
80 | 73, 79 | imbi12d 327 |
. . . . . . 7
  supp    g                         
  supp  g   supp
    

           supp 
          |
81 | 80 | imbi2d 323 |
. . . . . 6
  supp     g                          
   supp  g   supp
    

           supp 
           |
82 | | mplcoe1.i |
. . . . . . . . 9
   |
83 | | mplcoe1.r |
. . . . . . . . . 10
   |
84 | | ringgrp 17863 |
. . . . . . . . . 10

  |
85 | 83, 84 | syl 17 |
. . . . . . . . 9
   |
86 | 1, 4, 17, 44, 82, 85 | mpl0 18742 |
. . . . . . . 8
         |
87 | | fconstmpt 4883 |
. . . . . . . 8
    |
88 | 86, 87 | syl6eq 2521 |
. . . . . . 7
        |
89 | 88 | a1d 25 |
. . . . . 6
 
        |
90 | | ssun1 3588 |
. . . . . . . . . . 11

    |
91 | | sstr2 3425 |
. . . . . . . . . . 11
         
   |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . 10
    
  |
93 | 92 | imim1i 59 |
. . . . . . . . 9
 
 g                                g                            |
94 | | oveq1 6315 |
. . . . . . . . . . . 12
  g                        
  g                                                              |
95 | | eqid 2471 |
. . . . . . . . . . . . . 14
       |
96 | 1 | mplring 18753 |
. . . . . . . . . . . . . . . . 17
 

  |
97 | 82, 83, 96 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
   |
98 | | ringcmn 17889 |
. . . . . . . . . . . . . . . 16

CMnd |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . 15
 CMnd |
100 | 99 | adantr 472 |
. . . . . . . . . . . . . 14
 
 

      CMnd |
101 | | simprll 780 |
. . . . . . . . . . . . . 14
 
 

        |
102 | | simprr 774 |
. . . . . . . . . . . . . . . . 17
 
 

            |
103 | 102 | unssad 3602 |
. . . . . . . . . . . . . . . 16
 
 

        |
104 | 103 | sselda 3418 |
. . . . . . . . . . . . . . 15
     
      
  |
105 | 82 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
   |
106 | 83 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
   |
107 | 1 | mpllmod 18752 |
. . . . . . . . . . . . . . . . . 18
 

  |
108 | 105, 106,
107 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
   |
109 | 6 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . 18
 
           |
110 | 1, 82, 83 | mplsca 18746 |
. . . . . . . . . . . . . . . . . . . 20
 Scalar    |
111 | 110 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
 
 Scalar    |
112 | 111 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
 
        Scalar     |
113 | 109, 112 | eleqtrd 2551 |
. . . . . . . . . . . . . . . . 17
 
        Scalar     |
114 | | mplcoe1.o |
. . . . . . . . . . . . . . . . . 18
     |
115 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
 
   |
116 | 1, 3, 17, 114, 4, 105, 106, 115 | mplmon 18764 |
. . . . . . . . . . . . . . . . 17
 
        |
117 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
Scalar  Scalar   |
118 | | mplcoe1.n |
. . . . . . . . . . . . . . . . . 18
     |
119 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
   Scalar      Scalar    |
120 | 3, 117, 118, 119 | lmodvscl 18186 |
. . . . . . . . . . . . . . . . 17
         Scalar        
             |
121 | 108, 113,
116, 120 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
 
     

       |
122 | 121 | adantlr 729 |
. . . . . . . . . . . . . . 15
     
      
             |
123 | 104, 122 | syldan 478 |
. . . . . . . . . . . . . 14
     
      
             |
124 | | vex 3034 |
. . . . . . . . . . . . . . 15
 |
125 | 124 | a1i 11 |
. . . . . . . . . . . . . 14
 
 

        |
126 | | simprlr 781 |
. . . . . . . . . . . . . 14
 
 

     
  |
127 | 82, 83, 107 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
   |
128 | 127 | adantr 472 |
. . . . . . . . . . . . . . 15
 
 

        |
129 | 6 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
 

                |
130 | 102 | unssbd 3603 |
. . . . . . . . . . . . . . . . . 18
 
 

          |
131 | 124 | snss 4087 |
. . . . . . . . . . . . . . . . . 18

    |
132 | 130, 131 | sylibr 217 |
. . . . . . . . . . . . . . . . 17
 
 

        |
133 | 129, 132 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . 16
 
 

                |
134 | 110 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
 

      Scalar    |
135 | 134 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
 
 

             Scalar     |
136 | 133, 135 | eleqtrd 2551 |
. . . . . . . . . . . . . . 15
 
 

             Scalar     |
137 | 82 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
 

        |
138 | 83 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
 

        |
139 | 1, 3, 17, 114, 4, 137, 138, 132 | mplmon 18764 |
. . . . . . . . . . . . . . 15
 
 

             |
140 | 3, 117, 118, 119 | lmodvscl 18186 |
. . . . . . . . . . . . . . 15
         Scalar        
             |
141 | 128, 136,
139, 140 | syl3anc 1292 |
. . . . . . . . . . . . . 14
 
 

                   |
142 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
143 | | equequ2 1876 |
. . . . . . . . . . . . . . . . 17
 
   |
144 | 143 | ifbid 3894 |
. . . . . . . . . . . . . . . 16
   
     |
145 | 144 | mpteq2dv 4483 |
. . . . . . . . . . . . . . 15
             |
146 | 142, 145 | oveq12d 6326 |
. . . . . . . . . . . . . 14
     

         

       |
147 | 3, 95, 100, 101, 123, 125, 126, 141, 146 | gsumunsn 17670 |
. . . . . . . . . . . . 13
 
 

       g                     g                                  |
148 | | eqid 2471 |
. . . . . . . . . . . . . . 15
       |
149 | 129 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . 20
     
      
          |
150 | 2, 17 | ring0cl 17880 |
. . . . . . . . . . . . . . . . . . . . . 22

      |
151 | 83, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
       |
152 | 151 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
     
      
      |
153 | 149, 152 | ifcld 3915 |
. . . . . . . . . . . . . . . . . . 19
     
      
              |
154 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
                     |
155 | 153, 154 | fmptd 6061 |
. . . . . . . . . . . . . . . . . 18
 
 

                          |
156 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . 19
     |
157 | 156, 15 | elmap 7518 |
. . . . . . . . . . . . . . . . . 18
               
                     |
158 | 155, 157 | sylibr 217 |
. . . . . . . . . . . . . . . . 17
 
 

                        |
159 | 33, 2, 4, 34, 137 | psrbas 18679 |
. . . . . . . . . . . . . . . . 17
 
 

          mPwSer       
   |
160 | 158, 159 | eleqtrrd 2552 |
. . . . . . . . . . . . . . . 16
 
 

                    mPwSer     |
161 | 15 | mptex 6152 |
. . . . . . . . . . . . . . . . . . 19
           |
162 | | funmpt 5625 |
. . . . . . . . . . . . . . . . . . 19
           |
163 | 161, 162,
19 | 3pm3.2i 1208 |
. . . . . . . . . . . . . . . . . 18
                       |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
 

                              |
165 | | eldifn 3545 |
. . . . . . . . . . . . . . . . . . . 20
  
  |
166 | 165 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
     
        
  |
167 | 166 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . 18
     
        
         |
168 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
 

        |
169 | 167, 168 | suppss2 6968 |
. . . . . . . . . . . . . . . . 17
 
 

                 supp
  |
170 | | suppssfifsupp 7916 |
. . . . . . . . . . . . . . . . 17
                        
           supp            
finSupp  |
171 | 164, 101,
169, 170 | syl12anc 1290 |
. . . . . . . . . . . . . . . 16
 
 

                finSupp  |
172 | 1, 33, 34, 17, 3 | mplelbas 18731 |
. . . . . . . . . . . . . . . 16
                          mPwSer             finSupp   |
173 | 160, 171,
172 | sylanbrc 677 |
. . . . . . . . . . . . . . 15
 
 

                  |
174 | 1, 3, 148, 95, 173, 141 | mpladd 18743 |
. . . . . . . . . . . . . 14
 
 

                                                                 |
175 | | ovex 6336 |
. . . . . . . . . . . . . . . 16
                |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . 15
     
      
                 |
177 | | eqidd 2472 |
. . . . . . . . . . . . . . 15
 
 

                            |
178 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
         |
179 | 1, 118, 2, 3, 178, 4, 133, 139 | mplvsca 18748 |
. . . . . . . . . . . . . . . 16
 
 

                                         |
180 | 133 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
      
          |
181 | 2, 114 | ringidcl 17879 |
. . . . . . . . . . . . . . . . . . . 20

      |
182 | 181, 150 | ifcld 3915 |
. . . . . . . . . . . . . . . . . . 19

         |
183 | 83, 182 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   
      |
184 | 183 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
     
      
         |
185 | | fconstmpt 4883 |
. . . . . . . . . . . . . . . . . 18
               |
186 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
 

                      |
187 | | eqidd 2472 |
. . . . . . . . . . . . . . . . 17
 
 

                  |
188 | 168, 180,
184, 186, 187 | offval2 6567 |
. . . . . . . . . . . . . . . 16
 
 

                                               |
189 | 179, 188 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
 
 

                                    |
190 | 168, 153,
176, 177, 189 | offval2 6567 |
. . . . . . . . . . . . . 14
 
 

                                              
                      |
191 | 138, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
 

        |
192 | 2, 148, 17 | grplid 16774 |
. . . . . . . . . . . . . . . . . . . 20
                          |
193 | 191, 133,
192 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
 
 

                     |
194 | 193 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
     
                          |
195 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
     
               |
196 | | elsn 3973 |
. . . . . . . . . . . . . . . . . . . 20
     |
197 | 195, 196 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
     
             |
198 | 197 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
     
                     |
199 | 194, 198 | eqtr4d 2508 |
. . . . . . . . . . . . . . . . 17
     
                          |
200 | 126 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
     
          
  |
201 | 197, 200 | eqneltrd 2568 |
. . . . . . . . . . . . . . . . . . 19
     
          
  |
202 | 201 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . 18
     
                    |
203 | 197 | iftrued 3880 |
. . . . . . . . . . . . . . . . . . . 20
     
               |
204 | 203 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
     
                                      |
205 | 2, 178, 114 | ringridm 17883 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
206 | 138, 133,
205 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
 
 

                      |
207 | 206 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
     
                           |
208 | 204, 207 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
     
                                |
209 | 202, 208 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
     
                     
                              |
210 | | elun2 3593 |
. . . . . . . . . . . . . . . . . . 19
         |
211 | 210 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
     
                 |
212 | 211 | iftrued 3880 |
. . . . . . . . . . . . . . . . 17
     
                      
      |
213 | 199, 209,
212 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . . 16
     
                     
                                 |
214 | 85 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
     
      
  |
215 | 2, 148, 17 | grprid 16775 |
. . . . . . . . . . . . . . . . . . 19
         
                            |
216 | 214, 153,
215 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
     
      
                       |
217 | 216 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
       
                          |
218 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
  
    |
219 | 218, 196 | sylnib 311 |
. . . . . . . . . . . . . . . . . . . . 21
     
       
  
  |
220 | 219 | iffalsed 3883 |
. . . . . . . . . . . . . . . . . . . 20
     
       
     
 |
221 | 220 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
     
       
                              |
222 | 2, 178, 17 | ringrz 17896 |
. . . . . . . . . . . . . . . . . . . . 21
                      |
223 | 138, 133,
222 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
 
 

                 |
224 | 223 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
     
       
              |
225 | 221, 224 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
     
       
                   |
226 | 225 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
     
       
                                                |
227 | | biorf 412 |
. . . . . . . . . . . . . . . . . . . 20
  

  
    |
228 | | elun 3565 |
. . . . . . . . . . . . . . . . . . . . 21
     
     |
229 | | orcom 394 |
. . . . . . . . . . . . . . . . . . . . 21
    
  
   |
230 | 228, 229 | bitri 257 |
. . . . . . . . . . . . . . . . . . . 20
           |
231 | 227, 230 | syl6rbbr 272 |
. . . . . . . . . . . . . . . . . . 19
  
    
   |
232 | 231 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
     
       
           |
233 | 232 | ifbid 3894 |
. . . . . . . . . . . . . . . . 17
     
       
                         |
234 | 217, 226,
233 | 3eqtr4d 2515 |
. . . . . . . . . . . . . . . 16
     
       
                                               |
235 | 213, 234 | pm2.61dan 808 |
. . . . . . . . . . . . . . 15
     
      
                                            |
236 | 235 | mpteq2dva 4482 |
. . . . . . . . . . . . . 14
 
 

                 
                                    |
237 | 174, 190,
236 | 3eqtrrd 2510 |
. . . . . . . . . . . . 13
 
 

                                                  |
238 | 147, 237 | eqeq12d 2486 |
. . . . . . . . . . . 12
 
 

        g                                   g                                                               |
239 | 94, 238 | syl5ibr 229 |
. . . . . . . . . . 11
 
 

        g                        
 g                                    |
240 | 239 | expr 626 |
. . . . . . . . . 10
 
          g                        
 g                                     |
241 | 240 | a2d 28 |
. . . . . . . . 9
 
        
 g                                g                                     |
242 | 93, 241 | syl5 32 |
. . . . . . . 8
 
      g                                g                                     |
243 | 242 | expcom 442 |
. . . . . . 7
 

    g                                g                                      |
244 | 243 | a2d 28 |
. . . . . 6
 

    g                                  g                                      |
245 | 54, 63, 72, 81, 89, 244 | findcard2s 7830 |
. . . . 5
  supp
   supp
 g   supp                  supp
           |
246 | 38, 245 | mpcom 36 |
. . . 4
   supp  g   supp
    

           supp 
         |
247 | 32, 246 | mpd 15 |
. . 3
  g   supp
    

           supp 
        |
248 | 28, 247 | eqtr4d 2508 |
. 2
  g   supp
    

         |
249 | 32 | resmptd 5162 |
. . . 4
                supp    supp               |
250 | 249 | oveq2d 6324 |
. . 3
  g                supp    g   supp
    

         |
251 | | eqid 2471 |
. . . . 5
                           |
252 | 121, 251 | fmptd 6061 |
. . . 4
                    |
253 | 6, 13, 16, 20 | suppssr 6965 |
. . . . . . 7
 

 supp        |
254 | 253 | oveq1d 6323 |
. . . . . 6
 

 supp                      |
255 | | eldifi 3544 |
. . . . . . 7
   supp

  |
256 | 111 | fveq2d 5883 |
. . . . . . . . . 10
 
        Scalar     |
257 | 17, 256 | syl5eq 2517 |
. . . . . . . . 9
 
    Scalar     |
258 | 257 | oveq1d 6323 |
. . . . . . . 8
 
           Scalar  

       |
259 | | eqid 2471 |
. . . . . . . . . 10
   Scalar      Scalar    |
260 | 3, 117, 118, 259, 44 | lmod0vs 18202 |
. . . . . . . . 9
       
    Scalar               |
261 | 108, 116,
260 | syl2anc 673 |
. . . . . . . 8
 
     Scalar               |
262 | 258, 261 | eqtrd 2505 |
. . . . . . 7
 
             |
263 | 255, 262 | sylan2 482 |
. . . . . 6
 

 supp               |
264 | 254, 263 | eqtrd 2505 |
. . . . 5
 

 supp                    |
265 | 264, 16 | suppss2 6968 |
. . . 4
               supp       supp   |
266 | 15 | mptex 6152 |
. . . . . . 7
              |
267 | | funmpt 5625 |
. . . . . . 7
     

       |
268 | | fvex 5889 |
. . . . . . 7
     |
269 | 266, 267,
268 | 3pm3.2i 1208 |
. . . . . 6
      

     
                   |
270 | 269 | a1i 11 |
. . . . 5
                                   |
271 | | suppssfifsupp 7916 |
. . . . 5
                                    supp               supp       supp                finSupp       |
272 | 270, 38, 265, 271 | syl12anc 1290 |
. . . 4
              finSupp       |
273 | 3, 44, 99, 16, 252, 265, 272 | gsumres 17625 |
. . 3
  g                supp    g                 |
274 | 250, 273 | eqtr3d 2507 |
. 2
  g   supp
    

        g                 |
275 | 248, 274 | eqtrd 2505 |
1
  g                 |