Step | Hyp | Ref
| Expression |
1 | | mplmon.s |
. . 3
 mPoly   |
2 | | mplmon.b |
. . 3
     |
3 | | eqid 2462 |
. . 3
         |
4 | | mplmonmul.t |
. . 3
     |
5 | | mplmon.d |
. . 3
          |
6 | | mplmon.z |
. . . 4
     |
7 | | mplmon.o |
. . . 4
     |
8 | | mplmon.i |
. . . 4
   |
9 | | mplmon.r |
. . . 4
   |
10 | | mplmon.x |
. . . 4
   |
11 | 1, 2, 6, 7, 5, 8, 9, 10 | mplmon 18736 |
. . 3
        |
12 | | mplmonmul.x |
. . . 4
   |
13 | 1, 2, 6, 7, 5, 8, 9, 12 | mplmon 18736 |
. . 3
        |
14 | 1, 2, 3, 4, 5, 11,
13 | mplmul 18716 |
. 2
               g                                       |
15 | | eqeq1 2466 |
. . . . 5
           |
16 | 15 | ifbid 3915 |
. . . 4
               |
17 | 16 | cbvmptv 4509 |
. . 3
                 |
18 | | simpr 467 |
. . . . . . . . . 10
    
  


   |
19 | 18 | snssd 4130 |
. . . . . . . . 9
    
     

   |
20 | 19 | resmptd 5175 |
. . . . . . . 8
    
     
                               
                                      |
21 | 20 | oveq2d 6331 |
. . . . . . 7
    
    g   
                               
     g   
                                 |
22 | 9 | ad2antrr 737 |
. . . . . . . . 9
    
  
  |
23 | | ringmnd 17838 |
. . . . . . . . 9

  |
24 | 22, 23 | syl 17 |
. . . . . . . 8
    
  
  |
25 | 10 | ad2antrr 737 |
. . . . . . . 8
    
  
  |
26 | | iftrue 3899 |
. . . . . . . . . . . . 13
   
 |
27 | | eqid 2462 |
. . . . . . . . . . . . 13
           |
28 | | fvex 5898 |
. . . . . . . . . . . . . 14
     |
29 | 7, 28 | eqeltri 2536 |
. . . . . . . . . . . . 13
 |
30 | 26, 27, 29 | fvmpt 5971 |
. . . . . . . . . . . 12
           |
31 | 25, 30 | syl 17 |
. . . . . . . . . . 11
    
             |
32 | | ssrab2 3526 |
. . . . . . . . . . . . 13


  |
33 | 8 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    
  
  |
34 | | simplr 767 |
. . . . . . . . . . . . . 14
    
     |
35 | | eqid 2462 |
. . . . . . . . . . . . . . 15


  
  |
36 | 5, 35 | psrbagconcl 18646 |
. . . . . . . . . . . . . 14
 


 
 
 

   |
37 | 33, 34, 18, 36 | syl3anc 1276 |
. . . . . . . . . . . . 13
    
      
    |
38 | 32, 37 | sseldi 3442 |
. . . . . . . . . . . 12
    
        |
39 | | eqeq1 2466 |
. . . . . . . . . . . . . 14
           |
40 | 39 | ifbid 3915 |
. . . . . . . . . . . . 13
               |
41 | | eqid 2462 |
. . . . . . . . . . . . 13
           |
42 | | fvex 5898 |
. . . . . . . . . . . . . . 15
     |
43 | 6, 42 | eqeltri 2536 |
. . . . . . . . . . . . . 14
 |
44 | 29, 43 | ifex 3961 |
. . . . . . . . . . . . 13
     
 |
45 | 40, 41, 44 | fvmpt 5971 |
. . . . . . . . . . . 12
                        |
46 | 38, 45 | syl 17 |
. . . . . . . . . . 11
    
                       |
47 | 31, 46 | oveq12d 6333 |
. . . . . . . . . 10
    
                                              |
48 | | eqid 2462 |
. . . . . . . . . . . . . 14
         |
49 | 48, 7 | ringidcl 17850 |
. . . . . . . . . . . . 13

      |
50 | 48, 6 | ring0cl 17851 |
. . . . . . . . . . . . 13

      |
51 | 49, 50 | ifcld 3936 |
. . . . . . . . . . . 12

     
      |
52 | 22, 51 | syl 17 |
. . . . . . . . . . 11
    
               |
53 | 48, 3, 7 | ringlidm 17853 |
. . . . . . . . . . 11
            
                    |
54 | 22, 52, 53 | syl2anc 671 |
. . . . . . . . . 10
    
                       |
55 | 5 | psrbagf 18638 |
. . . . . . . . . . . . . . . . . 18
 
       |
56 | 33, 34, 55 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
    
         |
57 | 56 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . 16
   



         |
58 | 8 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
 
   |
59 | 10 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
 
   |
60 | 5 | psrbagf 18638 |
. . . . . . . . . . . . . . . . . . 19
 
       |
61 | 58, 59, 60 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
 
       |
62 | 61 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . 17
           |
63 | 62 | adantlr 726 |
. . . . . . . . . . . . . . . 16
   



         |
64 | 5 | psrbagf 18638 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
65 | 8, 12, 64 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
       |
66 | 65 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
 
       |
67 | 66 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . 17
           |
68 | 67 | adantlr 726 |
. . . . . . . . . . . . . . . 16
   



         |
69 | | nn0cn 10908 |
. . . . . . . . . . . . . . . . 17
    
      |
70 | | nn0cn 10908 |
. . . . . . . . . . . . . . . . 17
    
      |
71 | | nn0cn 10908 |
. . . . . . . . . . . . . . . . 17
    
      |
72 | | subadd 9904 |
. . . . . . . . . . . . . . . . 17
                             
                 |
73 | 69, 70, 71, 72 | syl3an 1318 |
. . . . . . . . . . . . . . . 16
         
                   
                 |
74 | 57, 63, 68, 73 | syl3anc 1276 |
. . . . . . . . . . . . . . 15
   



                 
                 |
75 | | eqcom 2469 |
. . . . . . . . . . . . . . 15
              
                |
76 | 74, 75 | syl6bb 269 |
. . . . . . . . . . . . . 14
   



                 
                 |
77 | 76 | ralbidva 2836 |
. . . . . . . . . . . . 13
    
                  

                 |
78 | | mpteqb 5987 |
. . . . . . . . . . . . . 14
 
                                               |
79 | | ovex 6343 |
. . . . . . . . . . . . . . 15
           |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
             |
81 | 78, 80 | mprg 2763 |
. . . . . . . . . . . . 13
                   
                |
82 | | mpteqb 5987 |
. . . . . . . . . . . . . 14
 
   
                   
                 |
83 | | fvex 5898 |
. . . . . . . . . . . . . . 15
     |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . 14
       |
85 | 82, 84 | mprg 2763 |
. . . . . . . . . . . . 13
                   
                |
86 | 77, 81, 85 | 3bitr4g 296 |
. . . . . . . . . . . 12
    
                                           |
87 | 56 | feqmptd 5941 |
. . . . . . . . . . . . . 14
    
           |
88 | 61 | feqmptd 5941 |
. . . . . . . . . . . . . . 15
 
         |
89 | 88 | adantr 471 |
. . . . . . . . . . . . . 14
    
  

       |
90 | 33, 57, 63, 87, 89 | offval2 6575 |
. . . . . . . . . . . . 13
    
                    |
91 | 66 | feqmptd 5941 |
. . . . . . . . . . . . . 14
 
         |
92 | 91 | adantr 471 |
. . . . . . . . . . . . 13
    
  

       |
93 | 90, 92 | eqeq12d 2477 |
. . . . . . . . . . . 12
    
      

                    |
94 | 58, 62, 67, 88, 91 | offval2 6575 |
. . . . . . . . . . . . . 14
 
                  |
95 | 94 | adantr 471 |
. . . . . . . . . . . . 13
    
                    |
96 | 87, 95 | eqeq12d 2477 |
. . . . . . . . . . . 12
    
      

                    |
97 | 86, 93, 96 | 3bitr4d 293 |
. . . . . . . . . . 11
    
      

     |
98 | 97 | ifbid 3915 |
. . . . . . . . . 10
    
                 |
99 | 47, 54, 98 | 3eqtrd 2500 |
. . . . . . . . 9
    
                                        |
100 | 98, 52 | eqeltrrd 2541 |
. . . . . . . . 9
    
               |
101 | 99, 100 | eqeltrd 2540 |
. . . . . . . 8
    
                                      |
102 | | fveq2 5888 |
. . . . . . . . . 10
                     |
103 | | oveq2 6323 |
. . . . . . . . . . 11
         |
104 | 103 | fveq2d 5892 |
. . . . . . . . . 10
                           |
105 | 102, 104 | oveq12d 6333 |
. . . . . . . . 9
                                                             |
106 | 48, 105 | gsumsn 17636 |
. . . . . . . 8
 
                                   g   
                                                              |
107 | 24, 25, 101, 106 | syl3anc 1276 |
. . . . . . 7
    
    g   
                                                              |
108 | 21, 107, 99 | 3eqtrd 2500 |
. . . . . 6
    
    g   
                               
            |
109 | 6 | gsum0 16570 |
. . . . . . 7
 g   |
110 | | disjsn 4044 |
. . . . . . . . 9
  
    


   |
111 | 9 | ad2antrr 737 |
. . . . . . . . . . . . 13
    
  
  |
112 | 1, 48, 2, 5, 11 | mplelf 18706 |
. . . . . . . . . . . . . . 15
                |
113 | 112 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    
                  |
114 | | simpr 467 |
. . . . . . . . . . . . . . 15
    
   

   |
115 | 32, 114 | sseldi 3442 |
. . . . . . . . . . . . . 14
    
     |
116 | 113, 115 | ffvelrnd 6046 |
. . . . . . . . . . . . 13
    
                  |
117 | 1, 48, 2, 5, 13 | mplelf 18706 |
. . . . . . . . . . . . . . 15
                |
118 | 117 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    
                  |
119 | 8 | ad2antrr 737 |
. . . . . . . . . . . . . . . 16
    
  
  |
120 | | simplr 767 |
. . . . . . . . . . . . . . . 16
    
     |
121 | 5, 35 | psrbagconcl 18646 |
. . . . . . . . . . . . . . . 16
 


 
 
 

   |
122 | 119, 120,
114, 121 | syl3anc 1276 |
. . . . . . . . . . . . . . 15
    
      
    |
123 | 32, 122 | sseldi 3442 |
. . . . . . . . . . . . . 14
    
        |
124 | 118, 123 | ffvelrnd 6046 |
. . . . . . . . . . . . 13
    
                     |
125 | 48, 3 | ringcl 17843 |
. . . . . . . . . . . . 13
                                                                   |
126 | 111, 116,
124, 125 | syl3anc 1276 |
. . . . . . . . . . . 12
    
                                      |
127 | | eqid 2462 |
. . . . . . . . . . . 12
  
                                

                                |
128 | 126, 127 | fmptd 6069 |
. . . . . . . . . . 11
 
  

                                            |
129 | | ffn 5751 |
. . . . . . . . . . 11
  

                                         
 
                                

   |
130 | | fnresdisj 5708 |
. . . . . . . . . . 11
  

                                         
  

                                     |
131 | 128, 129,
130 | 3syl 18 |
. . . . . . . . . 10
 
    
   
   
                                     |
132 | 131 | biimpa 491 |
. . . . . . . . 9
     
         
                                    |
133 | 110, 132 | sylan2br 483 |
. . . . . . . 8
   


 
  

                                    |
134 | 133 | oveq2d 6331 |
. . . . . . 7
   


 
 g                                   
     g    |
135 | 62 | nn0red 10955 |
. . . . . . . . . . . . . 14
           |
136 | | nn0addge1 10945 |
. . . . . . . . . . . . . 14
              
            |
137 | 135, 67, 136 | syl2anc 671 |
. . . . . . . . . . . . 13
                     |
138 | 137 | ralrimiva 2814 |
. . . . . . . . . . . 12
 
 
                |
139 | | ovex 6343 |
. . . . . . . . . . . . . 14
           |
140 | 139 | a1i 11 |
. . . . . . . . . . . . 13
                 |
141 | 58, 62, 140, 88, 94 | ofrfval2 6576 |
. . . . . . . . . . . 12
 
          
             |
142 | 138, 141 | mpbird 240 |
. . . . . . . . . . 11
 
 
     |
143 | | breq1 4419 |
. . . . . . . . . . . 12
     
  
    |
144 | 143 | elrab 3208 |
. . . . . . . . . . 11
  
 
 

  
    |
145 | 59, 142, 144 | sylanbrc 675 |
. . . . . . . . . 10
 
 
       |
146 | | breq2 4420 |
. . . . . . . . . . . 12
  
  
  
    |
147 | 146 | rabbidv 3048 |
. . . . . . . . . . 11
  
 
          |
148 | 147 | eleq2d 2525 |
. . . . . . . . . 10
  
     

       |
149 | 145, 148 | syl5ibrcom 230 |
. . . . . . . . 9
 
    
      |
150 | 149 | con3dimp 447 |
. . . . . . . 8
   


 
 
   |
151 | 150 | iffalsed 3904 |
. . . . . . 7
   


 
     
 |
152 | 109, 134,
151 | 3eqtr4a 2522 |
. . . . . 6
   


 
 g                                   
            |
153 | 108, 152 | pm2.61dan 805 |
. . . . 5
 
  g   
                               
            |
154 | 9 | adantr 471 |
. . . . . . 7
 
   |
155 | | ringcmn 17860 |
. . . . . . 7

CMnd |
156 | 154, 155 | syl 17 |
. . . . . 6
 
 CMnd |
157 | 5 | psrbaglefi 18645 |
. . . . . . 7
 
 
    |
158 | 8, 157 | sylan 478 |
. . . . . 6
 
 

   |
159 | | ssdif 3580 |
. . . . . . . . . . . 12
     
           |
160 | 32, 159 | ax-mp 5 |
. . . . . . . . . . 11
      
     |
161 | 160 | sseli 3440 |
. . . . . . . . . 10
  

   

     |
162 | 112 | adantr 471 |
. . . . . . . . . . 11
 
                |
163 | | eldifsni 4111 |
. . . . . . . . . . . . . . 15
       |
164 | 163 | adantl 472 |
. . . . . . . . . . . . . 14
           |
165 | 164 | neneqd 2640 |
. . . . . . . . . . . . 13
        
  |
166 | 165 | iffalsed 3904 |
. . . . . . . . . . . 12
           
 |
167 | | ovex 6343 |
. . . . . . . . . . . . . 14
   |
168 | 5, 167 | rabex2 4570 |
. . . . . . . . . . . . 13
 |
169 | 168 | a1i 11 |
. . . . . . . . . . . 12
 
   |
170 | 166, 169 | suppss2 6976 |
. . . . . . . . . . 11
 
       supp     |
171 | 43 | a1i 11 |
. . . . . . . . . . 11
 
   |
172 | 162, 170,
169, 171 | suppssr 6973 |
. . . . . . . . . 10
                   |
173 | 161, 172 | sylan2 481 |
. . . . . . . . 9
      
    
          |
174 | 173 | oveq1d 6330 |
. . . . . . . 8
      
    
                                                 |
175 | | eldifi 3567 |
. . . . . . . . 9
  

   
     |
176 | 48, 3, 6 | ringlz 17866 |
. . . . . . . . . 10
                                      |
177 | 111, 124,
176 | syl2anc 671 |
. . . . . . . . 9
    
                      |
178 | 175, 177 | sylan2 481 |
. . . . . . . 8
      
    
                   |
179 | 174, 178 | eqtrd 2496 |
. . . . . . 7
      
    
                              |
180 | 168 | rabex 4568 |
. . . . . . . 8


  |
181 | 180 | a1i 11 |
. . . . . . 7
 
 

   |
182 | 179, 181 | suppss2 6976 |
. . . . . 6
 
                                    supp
    |
183 | 168 | mptrabex 6162 |
. . . . . . . . 9
  
                                |
184 | | funmpt 5637 |
. . . . . . . . 9
 

                                |
185 | 183, 184,
43 | 3pm3.2i 1192 |
. . . . . . . 8
  

                                
                                  |
186 | 185 | a1i 11 |
. . . . . . 7
 
                                                                         |
187 | | snfi 7676 |
. . . . . . . 8
 
 |
188 | 187 | a1i 11 |
. . . . . . 7
 
  
  |
189 | | suppssfifsupp 7924 |
. . . . . . 7
    
                                                                  
     
                                supp
     
                                finSupp
 |
190 | 186, 188,
182, 189 | syl12anc 1274 |
. . . . . 6
 
  

                               finSupp  |
191 | 48, 6, 156, 158, 128, 182, 190 | gsumres 17596 |
. . . . 5
 
  g   
                               
     g                                      |
192 | 153, 191 | eqtr3d 2498 |
. . . 4
 
        g                                      |
193 | 192 | mpteq2dva 4503 |
. . 3
           g                                       |
194 | 17, 193 | syl5eq 2508 |
. 2
           g                                       |
195 | 14, 194 | eqtr4d 2499 |
1
                       |