Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . . 8
 mPoly   |
2 | | mdegmulle2.b |
. . . . . . . 8
     |
3 | | eqid 2622 |
. . . . . . . 8
         |
4 | | mdegmulle2.t |
. . . . . . . 8
     |
5 | | mdegmullem.a |
. . . . . . . 8
          |
6 | | mdegmulle2.f |
. . . . . . . 8
   |
7 | | mdegmulle2.g |
. . . . . . . 8
   |
8 | 1, 2, 3, 4, 5, 6, 7 | mplmul 19443 |
. . . . . . 7
     g                             |
9 | 8 | fveq1d 6193 |
. . . . . 6
          g                                |
10 | 9 | adantr 481 |
. . . . 5
 


                g                                |
11 | | breq2 4657 |
. . . . . . . . . 10
       |
12 | 11 | rabbidv 3189 |
. . . . . . . . 9
   


   |
13 | | oveq1 6657 |
. . . . . . . . . . 11
         |
14 | 13 | fveq2d 6195 |
. . . . . . . . . 10
     
           |
15 | 14 | oveq2d 6666 |
. . . . . . . . 9
                                         |
16 | 12, 15 | mpteq12dv 4733 |
. . . . . . . 8
                           
                       |
17 | 16 | oveq2d 6666 |
. . . . . . 7
  g                           g    
              
        |
18 | | eqid 2622 |
. . . . . . 7
  g                             g   
                        |
19 | | ovex 6678 |
. . . . . . 7
 g    
              
       |
20 | 17, 18, 19 | fvmpt 6282 |
. . . . . 6
    g                               g    
              
        |
21 | 20 | ad2antrl 764 |
. . . . 5
 


          g   
                           g    
              
        |
22 | | mdegaddle.d |
. . . . . . . . . . . . 13
 mDeg   |
23 | | eqid 2622 |
. . . . . . . . . . . . 13
         |
24 | | mdegmullem.h |
. . . . . . . . . . . . 13
 ℂfld g    |
25 | 6 | ad2antrr 762 |
. . . . . . . . . . . . 13
    

       
       
  |
26 | | elrabi 3359 |
. . . . . . . . . . . . . . 15
  
   |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . 14
    

            |
28 | 27 | adantrr 753 |
. . . . . . . . . . . . 13
    

       
          |
29 | 22, 1, 2 | mdegxrcl 23827 |
. . . . . . . . . . . . . . . . . 18
       |
30 | 6, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
31 | 30 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
    

                |
32 | | nn0ssre 11296 |
. . . . . . . . . . . . . . . . . . 19
 |
33 | | ressxr 10083 |
. . . . . . . . . . . . . . . . . . 19
 |
34 | 32, 33 | sstri 3612 |
. . . . . . . . . . . . . . . . . 18
 |
35 | | mdegmulle2.j1 |
. . . . . . . . . . . . . . . . . 18
   |
36 | 34, 35 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
   |
37 | 36 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
    

            |
38 | | mdegaddle.i |
. . . . . . . . . . . . . . . . . . . 20
   |
39 | 5, 24 | tdeglem1 23818 |
. . . . . . . . . . . . . . . . . . . 20
       |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
       |
41 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
    

                |
42 | 41, 27 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
    

                |
43 | 34, 42 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
    

                |
44 | 31, 37, 43 | 3jca 1242 |
. . . . . . . . . . . . . . 15
    

                      |
45 | 44 | adantrr 753 |
. . . . . . . . . . . . . 14
    

       
                    |
46 | | mdegmulle2.j2 |
. . . . . . . . . . . . . . . . 17
    
  |
47 | 46 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
    

                |
48 | 47 | anim1i 592 |
. . . . . . . . . . . . . . 15
    
 
                   
       |
49 | 48 | anasss 679 |
. . . . . . . . . . . . . 14
    

       
            
       |
50 | | xrlelttr 11987 |
. . . . . . . . . . . . . 14
                
                |
51 | 45, 49, 50 | sylc 65 |
. . . . . . . . . . . . 13
    

       
           
      |
52 | 22, 1, 2, 23, 5, 24, 25, 28, 51 | mdeglt 23825 |
. . . . . . . . . . . 12
    

       
                  |
53 | 52 | oveq1d 6665 |
. . . . . . . . . . 11
    

       
                                                |
54 | | mdegaddle.r |
. . . . . . . . . . . . . 14
   |
55 | 54 | ad2antrr 762 |
. . . . . . . . . . . . 13
    

            |
56 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
         |
57 | 1, 56, 2, 5, 7 | mplelf 19433 |
. . . . . . . . . . . . . . 15
           |
58 | 57 | ad2antrr 762 |
. . . . . . . . . . . . . 14
    

                    |
59 | | ssrab2 3687 |
. . . . . . . . . . . . . . 15
    |
60 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
    

            |
61 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
    

            |
62 | | simpr 477 |
. . . . . . . . . . . . . . . 16
    

          
    |
63 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
  


  |
64 | 5, 63 | psrbagconcl 19373 |
. . . . . . . . . . . . . . . 16
 


 
 
      |
65 | 60, 61, 62, 64 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
    

                  |
66 | 59, 65 | sseldi 3601 |
. . . . . . . . . . . . . 14
    

               |
67 | 58, 66 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
    

              
        |
68 | 56, 3, 23 | ringlz 18587 |
. . . . . . . . . . . . 13
      
      
                         |
69 | 55, 67, 68 | syl2anc 693 |
. . . . . . . . . . . 12
    

                                   |
70 | 69 | adantrr 753 |
. . . . . . . . . . 11
    

       
                                 |
71 | 53, 70 | eqtrd 2656 |
. . . . . . . . . 10
    

       
                                 |
72 | 71 | anassrs 680 |
. . . . . . . . 9
    
 
                                        |
73 | 7 | ad2antrr 762 |
. . . . . . . . . . . . 13
    

       
          
  |
74 | 66 | adantrr 753 |
. . . . . . . . . . . . 13
    

       
          
 
   |
75 | 22, 1, 2 | mdegxrcl 23827 |
. . . . . . . . . . . . . . . . . 18
       |
76 | 7, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
77 | 76 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
    

                |
78 | | mdegmulle2.k1 |
. . . . . . . . . . . . . . . . . 18
   |
79 | 34, 78 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
   |
80 | 79 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
    

            |
81 | 41, 66 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
    

              
    |
82 | 34, 81 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
    

              
    |
83 | 77, 80, 82 | 3jca 1242 |
. . . . . . . . . . . . . . 15
    

                         |
84 | 83 | adantrr 753 |
. . . . . . . . . . . . . 14
    

       
          
    
          |
85 | | mdegmulle2.k2 |
. . . . . . . . . . . . . . . . 17
    
  |
86 | 85 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
    

                |
87 | 86 | anim1i 592 |
. . . . . . . . . . . . . . 15
    
 
                           
     |
88 | 87 | anasss 679 |
. . . . . . . . . . . . . 14
    

       
          
               |
89 | | xrlelttr 11987 |
. . . . . . . . . . . . . 14
                        
      
          |
90 | 84, 88, 89 | sylc 65 |
. . . . . . . . . . . . 13
    

       
          
        
    |
91 | 22, 1, 2, 23, 5, 24, 73, 74, 90 | mdeglt 23825 |
. . . . . . . . . . . 12
    

       
          
             |
92 | 91 | oveq2d 6666 |
. . . . . . . . . . 11
    

       
          
              
                      |
93 | 1, 56, 2, 5, 6 | mplelf 19433 |
. . . . . . . . . . . . . . 15
           |
94 | 93 | ad2antrr 762 |
. . . . . . . . . . . . . 14
    

                    |
95 | 94, 27 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
    

                    |
96 | 56, 3, 23 | ringrz 18588 |
. . . . . . . . . . . . 13
                                 |
97 | 55, 95, 96 | syl2anc 693 |
. . . . . . . . . . . 12
    

                                |
98 | 97 | adantrr 753 |
. . . . . . . . . . 11
    

       
          
                      |
99 | 92, 98 | eqtrd 2656 |
. . . . . . . . . 10
    

       
          
              
          |
100 | 99 | anassrs 680 |
. . . . . . . . 9
    
 
                                           |
101 | | simplrr 801 |
. . . . . . . . . 10
    

          
       |
102 | 42 | nn0red 11352 |
. . . . . . . . . . . . 13
    

                |
103 | 81 | nn0red 11352 |
. . . . . . . . . . . . 13
    

              
    |
104 | 35 | ad2antrr 762 |
. . . . . . . . . . . . . 14
    

            |
105 | 104 | nn0red 11352 |
. . . . . . . . . . . . 13
    

            |
106 | 78 | ad2antrr 762 |
. . . . . . . . . . . . . 14
    

            |
107 | 106 | nn0red 11352 |
. . . . . . . . . . . . 13
    

            |
108 | | le2add 10510 |
. . . . . . . . . . . . 13
               
           
                      |
109 | 102, 103,
105, 107, 108 | syl22anc 1327 |
. . . . . . . . . . . 12
    

                                     
    |
110 | 5, 24 | tdeglem3 23819 |
. . . . . . . . . . . . . . 15
 

       
                    |
111 | 60, 27, 66, 110 | syl3anc 1326 |
. . . . . . . . . . . . . 14
    

              
                    |
112 | 5 | psrbagf 19365 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
113 | 112 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
114 | 113 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
  

       |
115 | 114 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
  

       |
116 | 5 | psrbagf 19365 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
117 | 116 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
118 | 117 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
  

       |
119 | 118 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
  

       |
120 | 115, 119 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . 18
  

                       |
121 | 120 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . 17
 
                           |
122 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
 
   |
123 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . 18
  

       |
124 | | ovexd 6680 |
. . . . . . . . . . . . . . . . . 18
  

             |
125 | 113 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . 18
 
         |
126 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . 19
  

       |
127 | 117 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . 19
 
         |
128 | 122, 126,
123, 127, 125 | offval2 6914 |
. . . . . . . . . . . . . . . . . 18
 
                  |
129 | 122, 123,
124, 125, 128 | offval2 6914 |
. . . . . . . . . . . . . . . . 17
 
                           |
130 | 121, 129,
127 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . 16
 
         |
131 | 60, 27, 61, 130 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
    

            
     |
132 | 131 | fveq2d 6195 |
. . . . . . . . . . . . . 14
    

              
           |
133 | 111, 132 | eqtr3d 2658 |
. . . . . . . . . . . . 13
    

                             |
134 | 133 | breq1d 4663 |
. . . . . . . . . . . 12
    

                              
    |
135 | 109, 134 | sylibd 229 |
. . . . . . . . . . 11
    

                                 |
136 | 102, 105 | lenltd 10183 |
. . . . . . . . . . . . 13
    

              
       |
137 | 103, 107 | lenltd 10183 |
. . . . . . . . . . . . 13
    

                      
     |
138 | 136, 137 | anbi12d 747 |
. . . . . . . . . . . 12
    

                       
        
       |
139 | | ioran 511 |
. . . . . . . . . . . 12
     
       
        
      |
140 | 138, 139 | syl6bbr 278 |
. . . . . . . . . . 11
    

                       
                |
141 | 41, 61 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
    

                |
142 | 141 | nn0red 11352 |
. . . . . . . . . . . 12
    

                |
143 | 35, 78 | nn0addcld 11355 |
. . . . . . . . . . . . . 14
     |
144 | 143 | ad2antrr 762 |
. . . . . . . . . . . . 13
    

          
   |
145 | 144 | nn0red 11352 |
. . . . . . . . . . . 12
    

          
   |
146 | 142, 145 | lenltd 10183 |
. . . . . . . . . . 11
    

              
 

        |
147 | 135, 140,
146 | 3imtr3d 282 |
. . . . . . . . . 10
    

               
        

       |
148 | 101, 147 | mt4d 152 |
. . . . . . . . 9
    

                         |
149 | 72, 100, 148 | mpjaodan 827 |
. . . . . . . 8
    

                                   |
150 | 149 | mpteq2dva 4744 |
. . . . . . 7
 


          
              
                |
151 | 150 | oveq2d 6666 |
. . . . . 6
 


        g    
              
       g    
        |
152 | | ringmnd 18556 |
. . . . . . . . 9

  |
153 | 54, 152 | syl 17 |
. . . . . . . 8
   |
154 | 153 | adantr 481 |
. . . . . . 7
 


      
  |
155 | | ovex 6678 |
. . . . . . . 8
   |
156 | 5, 155 | rab2ex 4816 |
. . . . . . 7
  
 |
157 | 23 | gsumz 17374 |
. . . . . . 7
    
  g   
             |
158 | 154, 156,
157 | sylancl 694 |
. . . . . 6
 


        g    
            |
159 | 151, 158 | eqtrd 2656 |
. . . . 5
 


        g    
              
            |
160 | 10, 21, 159 | 3eqtrd 2660 |
. . . 4
 


                   |
161 | 160 | expr 643 |
. . 3
 
   
                 |
162 | 161 | ralrimiva 2966 |
. 2
                      |
163 | 1 | mplring 19452 |
. . . . 5
 

  |
164 | 38, 54, 163 | syl2anc 693 |
. . . 4
   |
165 | 2, 4 | ringcl 18561 |
. . . 4
 
     |
166 | 164, 6, 7, 165 | syl3anc 1326 |
. . 3
     |
167 | 34, 143 | sseldi 3601 |
. . 3
     |
168 | 22, 1, 2, 23, 5, 24 | mdegleb 23824 |
. . 3
    
      
 
 

 
    
              |
169 | 166, 167,
168 | syl2anc 693 |
. 2
     
 
 

 
    
              |
170 | 162, 169 | mpbird 247 |
1
           |