Step | Hyp | Ref
| Expression |
1 | | mplcoe5.y |
. . . . . . . . 9
   |
2 | | mplcoe1.i |
. . . . . . . . . 10
   |
3 | | mplcoe1.d |
. . . . . . . . . . 11
          |
4 | 3 | psrbag 18588 |
. . . . . . . . . 10
 
              |
5 | 2, 4 | syl 17 |
. . . . . . . . 9
                |
6 | 1, 5 | mpbid 214 |
. . . . . . . 8
              |
7 | 6 | simpld 461 |
. . . . . . 7
       |
8 | 7 | feqmptd 5918 |
. . . . . 6
         |
9 | | iftrue 3887 |
. . . . . . . . 9
                          |
10 | 9 | adantl 468 |
. . . . . . . 8
                              |
11 | | eldif 3414 |
. . . . . . . . . 10
       

        |
12 | | ifid 3918 |
. . . . . . . . . . 11
                       |
13 | | frnnn0supp 10923 |
. . . . . . . . . . . . . . 15
        supp         |
14 | 2, 7, 13 | syl2anc 667 |
. . . . . . . . . . . . . 14
  supp         |
15 | | eqimss 3484 |
. . . . . . . . . . . . . 14
  supp      
 supp         |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . 13
  supp         |
17 | | c0ex 9637 |
. . . . . . . . . . . . . 14
 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . 13
   |
19 | 7, 16, 2, 18 | suppssr 6946 |
. . . . . . . . . . . 12
 

             |
20 | 19 | ifeq2d 3900 |
. . . . . . . . . . 11
 

                                         |
21 | 12, 20 | syl5reqr 2500 |
. . . . . . . . . 10
 

                           |
22 | 11, 21 | sylan2br 479 |
. . . . . . . . 9
 

                           |
23 | 22 | anassrs 654 |
. . . . . . . 8
   
                          |
24 | 10, 23 | pm2.61dan 800 |
. . . . . . 7
 
                     |
25 | 24 | mpteq2dva 4489 |
. . . . . 6
                         |
26 | 8, 25 | eqtr4d 2488 |
. . . . 5
                   |
27 | 26 | eqeq2d 2461 |
. . . 4
                     |
28 | 27 | ifbid 3903 |
. . 3
   
                     |
29 | 28 | mpteq2dv 4490 |
. 2
                             |
30 | | cnvimass 5188 |
. . . . 5
    
 |
31 | | fdm 5733 |
. . . . . 6
       |
32 | 7, 31 | syl 17 |
. . . . 5
   |
33 | 30, 32 | syl5sseq 3480 |
. . . 4
     
  |
34 | 6 | simprd 465 |
. . . . 5
     
  |
35 | | sseq1 3453 |
. . . . . . . 8


   |
36 | | noel 3735 |
. . . . . . . . . . . . . . . 16
 |
37 | | eleq2 2518 |
. . . . . . . . . . . . . . . 16


   |
38 | 36, 37 | mtbiri 305 |
. . . . . . . . . . . . . . 15

  |
39 | 38 | iffalsed 3892 |
. . . . . . . . . . . . . 14

           |
40 | 39 | mpteq2dv 4490 |
. . . . . . . . . . . . 13

               |
41 | | fconstmpt 4878 |
. . . . . . . . . . . . 13
       |
42 | 40, 41 | syl6eqr 2503 |
. . . . . . . . . . . 12

                 |
43 | 42 | eqeq2d 2461 |
. . . . . . . . . . 11

                   |
44 | 43 | ifbid 3903 |
. . . . . . . . . 10

             
         |
45 | 44 | mpteq2dv 4490 |
. . . . . . . . 9

                           |
46 | | mpteq1 4483 |
. . . . . . . . . . . 12

                          |
47 | | mpt0 5705 |
. . . . . . . . . . . 12
             |
48 | 46, 47 | syl6eq 2501 |
. . . . . . . . . . 11

              |
49 | 48 | oveq2d 6306 |
. . . . . . . . . 10

 g               g    |
50 | | mplcoe2.g |
. . . . . . . . . . . 12
mulGrp   |
51 | | eqid 2451 |
. . . . . . . . . . . 12
         |
52 | 50, 51 | ringidval 17737 |
. . . . . . . . . . 11
         |
53 | 52 | gsum0 16521 |
. . . . . . . . . 10
 g       |
54 | 49, 53 | syl6eq 2501 |
. . . . . . . . 9

 g                    |
55 | 45, 54 | eqeq12d 2466 |
. . . . . . . 8

                  g             

               |
56 | 35, 55 | imbi12d 322 |
. . . . . . 7

 
                 g               
                 |
57 | 56 | imbi2d 318 |
. . . . . 6

                    g                                    |
58 | | sseq1 3453 |
. . . . . . . 8
 
   |
59 | | eleq2 2518 |
. . . . . . . . . . . . . 14
 
   |
60 | 59 | ifbid 3903 |
. . . . . . . . . . . . 13
                     |
61 | 60 | mpteq2dv 4490 |
. . . . . . . . . . . 12
                         |
62 | 61 | eqeq2d 2461 |
. . . . . . . . . . 11
                           |
63 | 62 | ifbid 3903 |
. . . . . . . . . 10
                               |
64 | 63 | mpteq2dv 4490 |
. . . . . . . . 9
                                   |
65 | | mpteq1 4483 |
. . . . . . . . . 10
      
                    |
66 | 65 | oveq2d 6306 |
. . . . . . . . 9
  g               g                |
67 | 64, 66 | eqeq12d 2466 |
. . . . . . . 8
                   g             

                g                 |
68 | 58, 67 | imbi12d 322 |
. . . . . . 7
                    g                                 g                  |
69 | 68 | imbi2d 318 |
. . . . . 6
  
                  g                 
                 g                   |
70 | | sseq1 3453 |
. . . . . . . 8
             |
71 | | eleq2 2518 |
. . . . . . . . . . . . . 14
             |
72 | 71 | ifbid 3903 |
. . . . . . . . . . . . 13
                             |
73 | 72 | mpteq2dv 4490 |
. . . . . . . . . . . 12
                                 |
74 | 73 | eqeq2d 2461 |
. . . . . . . . . . 11
                
                  |
75 | 74 | ifbid 3903 |
. . . . . . . . . 10
                  
                    |
76 | 75 | mpteq2dv 4490 |
. . . . . . . . 9
                                           |
77 | | mpteq1 4483 |
. . . . . . . . . 10
                                   |
78 | 77 | oveq2d 6306 |
. . . . . . . . 9
      g               g                    |
79 | 76, 78 | eqeq12d 2466 |
. . . . . . . 8
                       g             

                    g                     |
80 | 70, 79 | imbi12d 322 |
. . . . . . 7
                        g                                         g                      |
81 | 80 | imbi2d 318 |
. . . . . 6
                         g                                           g                       |
82 | | sseq1 3453 |
. . . . . . . 8
      
        |
83 | | eleq2 2518 |
. . . . . . . . . . . . . 14
      
        |
84 | 83 | ifbid 3903 |
. . . . . . . . . . . . 13
                               |
85 | 84 | mpteq2dv 4490 |
. . . . . . . . . . . 12
                                   |
86 | 85 | eqeq2d 2461 |
. . . . . . . . . . 11
                                     |
87 | 86 | ifbid 3903 |
. . . . . . . . . 10
                                         |
88 | 87 | mpteq2dv 4490 |
. . . . . . . . 9
                                             |
89 | | mpteq1 4483 |
. . . . . . . . . 10
           
           
             |
90 | 89 | oveq2d 6306 |
. . . . . . . . 9
       g               g                     |
91 | 88, 90 | eqeq12d 2466 |
. . . . . . . 8
                        g             

                     g                      |
92 | 82, 91 | imbi12d 322 |
. . . . . . 7
                         g                                           g                       |
93 | 92 | imbi2d 318 |
. . . . . 6
       
                  g                      
                      g                        |
94 | | mplcoe1.p |
. . . . . . . . 9
 mPoly   |
95 | | mplcoe1.z |
. . . . . . . . 9
     |
96 | | mplcoe1.o |
. . . . . . . . 9
     |
97 | | mplcoe5.r |
. . . . . . . . 9
   |
98 | 94, 3, 95, 96, 51, 2, 97 | mpl1 18668 |
. . . . . . . 8
                |
99 | 98 | eqcomd 2457 |
. . . . . . 7
                |
100 | 99 | a1d 26 |
. . . . . 6
 
                |
101 | | ssun1 3597 |
. . . . . . . . . . 11

    |
102 | | sstr2 3439 |
. . . . . . . . . . 11
         
   |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . 10
    
  |
104 | 103 | imim1i 60 |
. . . . . . . . 9
 
                 g                   
                 g                 |
105 | | oveq1 6297 |
. . . . . . . . . . . 12
                  g                                         
        g                                 |
106 | | eqid 2451 |
. . . . . . . . . . . . . . 15
         |
107 | 2 | adantr 467 |
. . . . . . . . . . . . . . 15
 
 

        |
108 | 97 | adantr 467 |
. . . . . . . . . . . . . . 15
 
 

        |
109 | 7 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
 

            |
110 | 109 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . 18
     
      
      |
111 | | 0nn0 10884 |
. . . . . . . . . . . . . . . . . 18
 |
112 | | ifcl 3923 |
. . . . . . . . . . . . . . . . . 18
     
            |
113 | 110, 111,
112 | sylancl 668 |
. . . . . . . . . . . . . . . . 17
     
      
           |
114 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
                       |
115 | 113, 114 | fmptd 6046 |
. . . . . . . . . . . . . . . 16
 
 

                       |
116 | | frnnn0supp 10923 |
. . . . . . . . . . . . . . . . . 18
                              supp                    |
117 | 107, 115,
116 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
 

                  supp                    |
118 | | simprll 772 |
. . . . . . . . . . . . . . . . . 18
 
 

        |
119 | | eldifn 3556 |
. . . . . . . . . . . . . . . . . . . . 21
  
  |
120 | 119 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
     
        
  |
121 | 120 | iffalsed 3892 |
. . . . . . . . . . . . . . . . . . 19
     
        
           |
122 | 121, 107 | suppss2 6949 |
. . . . . . . . . . . . . . . . . 18
 
 

                  supp    |
123 | | ssfi 7792 |
. . . . . . . . . . . . . . . . . 18
              supp  
            supp    |
124 | 118, 122,
123 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
 

                  supp    |
125 | 117, 124 | eqeltrrd 2530 |
. . . . . . . . . . . . . . . 16
 
 

                     
  |
126 | 3 | psrbag 18588 |
. . . . . . . . . . . . . . . . 17
                                                 |
127 | 107, 126 | syl 17 |
. . . . . . . . . . . . . . . 16
 
 

                 
                               
    |
128 | 115, 125,
127 | mpbir2and 933 |
. . . . . . . . . . . . . . 15
 
 

                   |
129 | | eqid 2451 |
. . . . . . . . . . . . . . 15
         |
130 | | ssun2 3598 |
. . . . . . . . . . . . . . . . . . 19
 
     |
131 | | simprr 766 |
. . . . . . . . . . . . . . . . . . 19
 
 

            |
132 | 130, 131 | syl5ss 3443 |
. . . . . . . . . . . . . . . . . 18
 
 

          |
133 | | vex 3048 |
. . . . . . . . . . . . . . . . . . 19
 |
134 | 133 | snss 4096 |
. . . . . . . . . . . . . . . . . 18

    |
135 | 132, 134 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
 
 

        |
136 | 109, 135 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
 
 

            |
137 | 3 | snifpsrbag 18590 |
. . . . . . . . . . . . . . . 16
                    |
138 | 107, 136,
137 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
 

                   |
139 | 94, 106, 95, 96, 3, 107, 108, 128, 129, 138 | mplmonmul 18688 |
. . . . . . . . . . . . . 14
 
 

                                                                              |
140 | | mplcoe2.m |
. . . . . . . . . . . . . . . 16
.g   |
141 | | mplcoe2.v |
. . . . . . . . . . . . . . . 16
 mVar   |
142 | 94, 3, 95, 96, 107, 50, 140, 141, 108, 135, 136 | mplcoe3 18690 |
. . . . . . . . . . . . . . 15
 
 

                          
       |
143 | 142 | oveq2d 6306 |
. . . . . . . . . . . . . 14
 
 

                                                                         
        |
144 | 136 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     
      
      |
145 | | ifcl 3923 |
. . . . . . . . . . . . . . . . . . . 20
     
            |
146 | 144, 111,
145 | sylancl 668 |
. . . . . . . . . . . . . . . . . . 19
     
      
           |
147 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . 19
 
 

                              |
148 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . 19
 
 

                              |
149 | 107, 113,
146, 147, 148 | offval2 6548 |
. . . . . . . . . . . . . . . . . 18
 
 

                                                       |
150 | 110 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                 |
151 | 150 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                 |
152 | 151 | addid2d 9834 |
. . . . . . . . . . . . . . . . . . . . 21
     
                       |
153 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
154 | 153 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
             |
155 | | simprlr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
 

     
  |
156 | 155 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
          
  |
157 | 154, 156 | eqneltrd 2548 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
          
  |
158 | 157 | iffalsed 3892 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                      |
159 | 154 | iftrued 3889 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                          |
160 | 154 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                     |
161 | 159, 160 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                          |
162 | 158, 161 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . 21
     
                                       |
163 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
               |
164 | 130, 163 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                 |
165 | 164 | iftrued 3889 |
. . . . . . . . . . . . . . . . . . . . 21
     
                              |
166 | 152, 162,
165 | 3eqtr4d 2495 |
. . . . . . . . . . . . . . . . . . . 20
     
                                              |
167 | 113 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
       
              |
168 | 167 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
              |
169 | 168 | addid1d 9833 |
. . . . . . . . . . . . . . . . . . . . 21
     
       
                         |
170 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
       
  
    |
171 | | elsn 3982 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
172 | 170, 171 | sylnib 306 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
       
  
  |
173 | 172 | iffalsed 3892 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
              |
174 | 173 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . 21
     
       
                                    |
175 | | biorf 407 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

  
    |
176 | | elun 3574 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
     |
177 | | orcom 389 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  
   |
178 | 176, 177 | bitri 253 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
179 | 175, 178 | syl6rbbr 268 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
    
   |
180 | 179 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
           |
181 | 180 | ifbid 3903 |
. . . . . . . . . . . . . . . . . . . . 21
     
       
                           |
182 | 169, 174,
181 | 3eqtr4d 2495 |
. . . . . . . . . . . . . . . . . . . 20
     
       
                                      |
183 | 166, 182 | pm2.61dan 800 |
. . . . . . . . . . . . . . . . . . 19
     
      
                                   |
184 | 183 | mpteq2dva 4489 |
. . . . . . . . . . . . . . . . . 18
 
 

                                             |
185 | 149, 184 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
 
 

                                                |
186 | 185 | eqeq2d 2461 |
. . . . . . . . . . . . . . . 16
 
 

                               
                  |
187 | 186 | ifbid 3903 |
. . . . . . . . . . . . . . 15
 
 

                                 
                    |
188 | 187 | mpteq2dv 4490 |
. . . . . . . . . . . . . 14
 
 

                                                          |
189 | 139, 143,
188 | 3eqtr3rd 2494 |
. . . . . . . . . . . . 13
 
 

                                                     
        |
190 | 50, 106 | mgpbas 17729 |
. . . . . . . . . . . . . 14
         |
191 | 50, 129 | mgpplusg 17727 |
. . . . . . . . . . . . . 14
        |
192 | | eqid 2451 |
. . . . . . . . . . . . . 14
Cntz  Cntz   |
193 | | eqid 2451 |
. . . . . . . . . . . . . 14
                                 |
194 | 94 | mplring 18676 |
. . . . . . . . . . . . . . . . 17
 

  |
195 | 2, 97, 194 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
   |
196 | 50 | ringmgp 17786 |
. . . . . . . . . . . . . . . 16

  |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . 15
   |
198 | 197 | adantr 467 |
. . . . . . . . . . . . . 14
 
 

        |
199 | 1 | adantr 467 |
. . . . . . . . . . . . . . 15
 
 

        |
200 | | mplcoe5.c |
. . . . . . . . . . . . . . . . 17
  
                                |
201 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . 20
           |
202 | 201 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . 19
                                 |
203 | 201 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
                                 |
204 | 202, 203 | eqeq12d 2466 |
. . . . . . . . . . . . . . . . . 18
                               
      
                          |
205 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . 20
           |
206 | 205 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
                                 |
207 | 205 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . 19
                                 |
208 | 206, 207 | eqeq12d 2466 |
. . . . . . . . . . . . . . . . . 18
                               
      
                          |
209 | 204, 208 | cbvral2v 3027 |
. . . . . . . . . . . . . . . . 17
 

                              

                                |
210 | 200, 209 | sylib 200 |
. . . . . . . . . . . . . . . 16
  
                                |
211 | 210 | adantr 467 |
. . . . . . . . . . . . . . 15
 
 

       
                                |
212 | 94, 3, 95, 96, 107, 50, 140, 141, 108, 199, 211, 131 | mplcoe5lem 18691 |
. . . . . . . . . . . . . 14
 
 

     
         
       Cntz                       |
213 | 101, 131 | syl5ss 3443 |
. . . . . . . . . . . . . . . 16
 
 

        |
214 | 213 | sselda 3432 |
. . . . . . . . . . . . . . 15
     
      
  |
215 | 197 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
   |
216 | 7 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . 17
 
       |
217 | 2 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
   |
218 | 97 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
   |
219 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
 
   |
220 | 94, 141, 106, 217, 218, 219 | mvrcl 18673 |
. . . . . . . . . . . . . . . . 17
 
           |
221 | 190, 140 | mulgnn0cl 16774 |
. . . . . . . . . . . . . . . . 17
     
             
           |
222 | 215, 216,
220, 221 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
 
     
           |
223 | 222 | adantlr 721 |
. . . . . . . . . . . . . . 15
     
      
                |
224 | 214, 223 | syldan 473 |
. . . . . . . . . . . . . 14
     
      
                |
225 | 94, 141, 106, 107, 108, 135 | mvrcl 18673 |
. . . . . . . . . . . . . . 15
 
 

                |
226 | 190, 140 | mulgnn0cl 16774 |
. . . . . . . . . . . . . . 15
     
             
           |
227 | 198, 136,
225, 226 | syl3anc 1268 |
. . . . . . . . . . . . . 14
 
 

                      |
228 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
229 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
230 | 228, 229 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
     
                 |
231 | 230 | adantl 468 |
. . . . . . . . . . . . . 14
     
      
              
       |
232 | 190, 191,
192, 193, 198, 118, 212, 224, 135, 155, 227, 231 | gsumzunsnd 17588 |
. . . . . . . . . . . . 13
 
 

       g                    g                                 |
233 | 189, 232 | eqeq12d 2466 |
. . . . . . . . . . . 12
 
 

                            g                                             
        g                                  |
234 | 105, 233 | syl5ibr 225 |
. . . . . . . . . . 11
 
 

                        g                                   g                     |
235 | 234 | expr 620 |
. . . . . . . . . 10
 
                          g                                   g                      |
236 | 235 | a2d 29 |
. . . . . . . . 9
 
        
                 g                   
                     g                      |
237 | 104, 236 | syl5 33 |
. . . . . . . 8
 
                      g                   
                     g                      |
238 | 237 | expcom 437 |
. . . . . . 7
 

                    g                   
                     g                       |
239 | 238 | a2d 29 |
. . . . . 6
 

                    g               
                           g                       |
240 | 57, 69, 81, 93, 100, 239 | findcard2s 7812 |
. . . . 5
                                   g                       |
241 | 34, 240 | mpcom 37 |
. . . 4
                             g                      |
242 | 33, 241 | mpd 15 |
. . 3
                       g                     |
243 | 33 | resmptd 5156 |
. . . 4
                                       |
244 | 243 | oveq2d 6306 |
. . 3
  g                      g                     |
245 | | eqid 2451 |
. . . . 5
                         |
246 | 222, 245 | fmptd 6046 |
. . . 4
                       |
247 | | ssid 3451 |
. . . . . 6
 |
248 | 247 | a1i 11 |
. . . . 5

  |
249 | 94, 3, 95, 96, 2, 50, 140, 141, 97, 1, 200, 248 | mplcoe5lem 18691 |
. . . 4
              Cntz                   |
250 | 7, 16, 2, 18 | suppssr 6946 |
. . . . . . 7
 

             |
251 | 250 | oveq1d 6305 |
. . . . . 6
 

           
             |
252 | | eldifi 3555 |
. . . . . . . 8
          |
253 | 252, 220 | sylan2 477 |
. . . . . . 7
 

                 |
254 | 190, 52, 140 | mulg0 16763 |
. . . . . . 7
        
            |
255 | 253, 254 | syl 17 |
. . . . . 6
 

       
           |
256 | 251, 255 | eqtrd 2485 |
. . . . 5
 

           
           |
257 | 256, 2 | suppss2 6949 |
. . . 4
              supp             |
258 | | mptexg 6135 |
. . . . . 6
      
        |
259 | 2, 258 | syl 17 |
. . . . 5
               |
260 | | funmpt 5618 |
. . . . . 6
     
       |
261 | 260 | a1i 11 |
. . . . 5
               |
262 | | fvex 5875 |
. . . . . 6
     |
263 | 262 | a1i 11 |
. . . . 5
       |
264 | | suppssfifsupp 7898 |
. . . . 5
                                     
             supp                         finSupp       |
265 | 259, 261,
263, 34, 257, 264 | syl32anc 1276 |
. . . 4
             finSupp
      |
266 | 190, 52, 192, 197, 2, 246, 249, 257, 265 | gsumzres 17543 |
. . 3
  g                      g                |
267 | 242, 244,
266 | 3eqtr2d 2491 |
. 2
                       g                |
268 | 29, 267 | eqtrd 2485 |
1
       g                |