Step | Hyp | Ref
| Expression |
1 | | elply 23149 |
. . . . 5
 Poly                                 |
2 | 1 | simprbi 466 |
. . . 4
 Poly 
                             |
3 | | eqid 2451 |
. . . . . . . . 9
ℂfld s  ℂfld s   |
4 | | cnfldbas 18974 |
. . . . . . . . 9
  ℂfld |
5 | | eqid 2451 |
. . . . . . . . 9
   ℂfld s      ℂfld s    |
6 | | cnex 9620 |
. . . . . . . . . 10
 |
7 | 6 | a1i 11 |
. . . . . . . . 9
  SubRing ℂfld

 
        |
8 | | fzfid 12186 |
. . . . . . . . 9
  SubRing ℂfld

 
            |
9 | | cnring 18990 |
. . . . . . . . . 10
ℂfld  |
10 | | ringcmn 17811 |
. . . . . . . . . 10
ℂfld ℂfld CMnd |
11 | 9, 10 | mp1i 13 |
. . . . . . . . 9
  SubRing ℂfld

 
      ℂfld CMnd |
12 | 4 | subrgss 18009 |
. . . . . . . . . . . . 13
 SubRing ℂfld
  |
13 | 12 | ad2antrr 732 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
       |
14 | | elmapi 7493 |
. . . . . . . . . . . . . . 15
                 |
15 | 14 | ad2antll 735 |
. . . . . . . . . . . . . 14
  SubRing ℂfld

 
                |
16 | | subrgsubg 18014 |
. . . . . . . . . . . . . . . . . . 19
 SubRing ℂfld
SubGrp ℂfld  |
17 | | cnfld0 18992 |
. . . . . . . . . . . . . . . . . . . 20
  ℂfld |
18 | 17 | subg0cl 16825 |
. . . . . . . . . . . . . . . . . . 19
 SubGrp ℂfld
  |
19 | 16, 18 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 SubRing ℂfld
  |
20 | 19 | adantr 467 |
. . . . . . . . . . . . . . . . 17
  SubRing ℂfld

 
        |
21 | 20 | snssd 4117 |
. . . . . . . . . . . . . . . 16
  SubRing ℂfld

 
          |
22 | | ssequn2 3607 |
. . . . . . . . . . . . . . . 16
         |
23 | 21, 22 | sylib 200 |
. . . . . . . . . . . . . . 15
  SubRing ℂfld

 
            |
24 | 23 | feq3d 5716 |
. . . . . . . . . . . . . 14
  SubRing ℂfld

 
              
       |
25 | 15, 24 | mpbid 214 |
. . . . . . . . . . . . 13
  SubRing ℂfld

 
            |
26 | | elfznn0 11887 |
. . . . . . . . . . . . 13
       |
27 | | ffvelrn 6020 |
. . . . . . . . . . . . 13
     
       |
28 | 25, 26, 27 | syl2an 480 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
           |
29 | 13, 28 | sseldd 3433 |
. . . . . . . . . . 11
   SubRing ℂfld 
       
           |
30 | 29 | adantrl 722 |
. . . . . . . . . 10
   SubRing ℂfld 
              
      |
31 | | simprl 764 |
. . . . . . . . . . 11
   SubRing ℂfld 
              
  |
32 | 26 | ad2antll 735 |
. . . . . . . . . . 11
   SubRing ℂfld 
              
  |
33 | | expcl 12290 |
. . . . . . . . . . 11
 
       |
34 | 31, 32, 33 | syl2anc 667 |
. . . . . . . . . 10
   SubRing ℂfld 
              
      |
35 | 30, 34 | mulcld 9663 |
. . . . . . . . 9
   SubRing ℂfld 
              
            |
36 | | eqid 2451 |
. . . . . . . . . 10
                                     |
37 | 6 | mptex 6136 |
. . . . . . . . . . 11
             |
38 | 37 | a1i 11 |
. . . . . . . . . 10
   SubRing ℂfld 
       
                   |
39 | | fvex 5875 |
. . . . . . . . . . 11
   ℂfld s    |
40 | 39 | a1i 11 |
. . . . . . . . . 10
  SubRing ℂfld

 
         ℂfld s     |
41 | 36, 8, 38, 40 | fsuppmptdm 7894 |
. . . . . . . . 9
  SubRing ℂfld

 
                        finSupp    ℂfld s     |
42 | 3, 4, 5, 7, 8, 11,
35, 41 | pwsgsum 17611 |
. . . . . . . 8
  SubRing ℂfld

 
       ℂfld s  g                     ℂfld g                     |
43 | | fzfid 12186 |
. . . . . . . . . 10
   SubRing ℂfld 
       
       |
44 | 35 | anassrs 654 |
. . . . . . . . . 10
    SubRing ℂfld

 
     

                 |
45 | 43, 44 | gsumfsum 19034 |
. . . . . . . . 9
   SubRing ℂfld 
       
 ℂfld g                                    |
46 | 45 | mpteq2dva 4489 |
. . . . . . . 8
  SubRing ℂfld

 
       ℂfld g                                       |
47 | 42, 46 | eqtrd 2485 |
. . . . . . 7
  SubRing ℂfld

 
       ℂfld s  g                                        |
48 | 3 | pwsring 17843 |
. . . . . . . . . 10
 ℂfld  ℂfld s    |
49 | 9, 6, 48 | mp2an 678 |
. . . . . . . . 9
ℂfld s   |
50 | | ringcmn 17811 |
. . . . . . . . 9
 ℂfld s 
ℂfld s  CMnd |
51 | 49, 50 | mp1i 13 |
. . . . . . . 8
  SubRing ℂfld

 
      ℂfld s 
CMnd |
52 | | cncrng 18989 |
. . . . . . . . . . 11
ℂfld  |
53 | | plypf1.e |
. . . . . . . . . . . 12
eval1 ℂfld |
54 | | eqid 2451 |
. . . . . . . . . . . 12
Poly1 ℂfld
Poly1 ℂfld |
55 | 53, 54, 3, 4 | evl1rhm 18920 |
. . . . . . . . . . 11
ℂfld
 Poly1 ℂfld RingHom ℂfld s     |
56 | 52, 55 | ax-mp 5 |
. . . . . . . . . 10
 Poly1 ℂfld RingHom ℂfld s    |
57 | | plypf1.r |
. . . . . . . . . . . 12
ℂfld ↾s   |
58 | | plypf1.p |
. . . . . . . . . . . 12
Poly1   |
59 | | plypf1.a |
. . . . . . . . . . . 12
     |
60 | 54, 57, 58, 59 | subrgply1 18826 |
. . . . . . . . . . 11
 SubRing ℂfld
SubRing Poly1 ℂfld   |
61 | 60 | adantr 467 |
. . . . . . . . . 10
  SubRing ℂfld

 
     
SubRing Poly1 ℂfld   |
62 | | rhmima 18039 |
. . . . . . . . . 10
   Poly1 ℂfld RingHom ℂfld s   SubRing Poly1 ℂfld      SubRing ℂfld s     |
63 | 56, 61, 62 | sylancr 669 |
. . . . . . . . 9
  SubRing ℂfld

 
          SubRing ℂfld s     |
64 | | subrgsubg 18014 |
. . . . . . . . 9
     SubRing ℂfld s  
    SubGrp ℂfld s     |
65 | | subgsubm 16839 |
. . . . . . . . 9
     SubGrp ℂfld s  
    SubMnd ℂfld s     |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . 8
  SubRing ℂfld

 
          SubMnd ℂfld s     |
67 | | eqid 2451 |
. . . . . . . . . . . 12
   ℂfld s      ℂfld s    |
68 | 9 | a1i 11 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
     ℂfld   |
69 | 6 | a1i 11 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
       |
70 | | fconst6g 5772 |
. . . . . . . . . . . . . 14
                   |
71 | 29, 70 | syl 17 |
. . . . . . . . . . . . 13
   SubRing ℂfld 
       
                   |
72 | 3, 4, 67 | pwselbasb 15386 |
. . . . . . . . . . . . . 14
 ℂfld              ℂfld s  
               |
73 | 9, 6, 72 | mp2an 678 |
. . . . . . . . . . . . 13
            ℂfld
s
                |
74 | 71, 73 | sylibr 216 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
                ℂfld s     |
75 | 34 | anass1rs 816 |
. . . . . . . . . . . . . 14
    SubRing ℂfld

 
     
            |
76 | | eqid 2451 |
. . . . . . . . . . . . . 14
             |
77 | 75, 76 | fmptd 6046 |
. . . . . . . . . . . . 13
   SubRing ℂfld 
       
                 |
78 | 3, 4, 67 | pwselbasb 15386 |
. . . . . . . . . . . . . 14
 ℂfld            ℂfld s                |
79 | 9, 6, 78 | mp2an 678 |
. . . . . . . . . . . . 13
          ℂfld s  
            |
80 | 77, 79 | sylibr 216 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
              ℂfld s     |
81 | | cnfldmul 18976 |
. . . . . . . . . . . 12
  ℂfld |
82 | | eqid 2451 |
. . . . . . . . . . . 12
   ℂfld s      ℂfld s    |
83 | 3, 67, 68, 69, 74, 80, 81, 82 | pwsmulrval 15389 |
. . . . . . . . . . 11
   SubRing ℂfld 
       
                  ℂfld s                              |
84 | 29 | adantr 467 |
. . . . . . . . . . . 12
    SubRing ℂfld

 
     
            |
85 | | fconstmpt 4878 |
. . . . . . . . . . . . 13
               |
86 | 85 | a1i 11 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
                     |
87 | | eqidd 2452 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
                   |
88 | 69, 84, 75, 86, 87 | offval2 6548 |
. . . . . . . . . . 11
   SubRing ℂfld 
       
                                    |
89 | 83, 88 | eqtrd 2485 |
. . . . . . . . . 10
   SubRing ℂfld 
       
                  ℂfld s                         |
90 | 63 | adantr 467 |
. . . . . . . . . . 11
   SubRing ℂfld 
       
         SubRing ℂfld s     |
91 | | eqid 2451 |
. . . . . . . . . . . . . 14
algSc Poly1 ℂfld algSc Poly1 ℂfld  |
92 | 53, 54, 4, 91 | evl1sca 18922 |
. . . . . . . . . . . . 13
 ℂfld          algSc Poly1 ℂfld                   |
93 | 52, 29, 92 | sylancr 669 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
         algSc Poly1 ℂfld                   |
94 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
   Poly1 ℂfld    Poly1 ℂfld  |
95 | 94, 67 | rhmf 17954 |
. . . . . . . . . . . . . . 15
  Poly1 ℂfld
RingHom ℂfld s        Poly1 ℂfld      ℂfld s     |
96 | 56, 95 | ax-mp 5 |
. . . . . . . . . . . . . 14
     Poly1 ℂfld      ℂfld s    |
97 | | ffn 5728 |
. . . . . . . . . . . . . 14
      Poly1 ℂfld      ℂfld s  
   Poly1 ℂfld   |
98 | 96, 97 | mp1i 13 |
. . . . . . . . . . . . 13
   SubRing ℂfld 
       
        Poly1 ℂfld   |
99 | 94 | subrgss 18009 |
. . . . . . . . . . . . . . 15
 SubRing Poly1 ℂfld
   Poly1 ℂfld   |
100 | 60, 99 | syl 17 |
. . . . . . . . . . . . . 14
 SubRing ℂfld
   Poly1 ℂfld   |
101 | 100 | ad2antrr 732 |
. . . . . . . . . . . . 13
   SubRing ℂfld 
       
        Poly1 ℂfld   |
102 | | simpll 760 |
. . . . . . . . . . . . . . 15
   SubRing ℂfld 
       
     SubRing ℂfld  |
103 | 54, 91, 57, 58, 102, 59, 4, 29 | subrg1asclcl 18853 |
. . . . . . . . . . . . . 14
   SubRing ℂfld 
       
       algSc Poly1 ℂfld       
       |
104 | 28, 103 | mpbird 236 |
. . . . . . . . . . . . 13
   SubRing ℂfld 
       
      algSc Poly1 ℂfld          |
105 | | fnfvima 6143 |
. . . . . . . . . . . . 13
     Poly1 ℂfld    Poly1 ℂfld
 algSc Poly1 ℂfld             algSc Poly1 ℂfld               |
106 | 98, 101, 104, 105 | syl3anc 1268 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
         algSc Poly1 ℂfld               |
107 | 93, 106 | eqeltrrd 2530 |
. . . . . . . . . . 11
   SubRing ℂfld 
       
                   |
108 | 67 | subrgss 18009 |
. . . . . . . . . . . . . . . . 17
     SubRing ℂfld s  
       ℂfld s     |
109 | 90, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
   SubRing ℂfld 
       
            ℂfld s     |
110 | 60 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
   SubRing ℂfld 
       
     SubRing Poly1 ℂfld   |
111 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . 20
mulGrp Poly1 ℂfld mulGrp Poly1 ℂfld  |
112 | 111 | subrgsubm 18021 |
. . . . . . . . . . . . . . . . . . 19
 SubRing Poly1 ℂfld
SubMnd mulGrp Poly1 ℂfld    |
113 | 110, 112 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   SubRing ℂfld 
       
     SubMnd mulGrp Poly1 ℂfld    |
114 | 26 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
   SubRing ℂfld 
       
       |
115 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
var1 ℂfld
var1 ℂfld |
116 | 115, 102,
57, 58, 59 | subrgvr1cl 18855 |
. . . . . . . . . . . . . . . . . 18
   SubRing ℂfld 
       
     var1 ℂfld   |
117 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
.g mulGrp Poly1 ℂfld  .g mulGrp Poly1 ℂfld   |
118 | 117 | submmulgcl 16792 |
. . . . . . . . . . . . . . . . . 18
  SubMnd mulGrp Poly1 ℂfld 
var1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld   |
119 | 113, 114,
116, 118 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
   SubRing ℂfld 
       
       .g mulGrp Poly1 ℂfld   var1 ℂfld   |
120 | | fnfvima 6143 |
. . . . . . . . . . . . . . . . 17
     Poly1 ℂfld    Poly1 ℂfld
  .g mulGrp Poly1 ℂfld   var1 ℂfld 
     .g mulGrp Poly1 ℂfld   var1 ℂfld        |
121 | 98, 101, 119, 120 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
   SubRing ℂfld 
       
          .g mulGrp Poly1 ℂfld   var1 ℂfld        |
122 | 109, 121 | sseldd 3433 |
. . . . . . . . . . . . . . 15
   SubRing ℂfld 
       
          .g mulGrp Poly1 ℂfld   var1 ℂfld     ℂfld
s
    |
123 | 3, 4, 67, 68, 69, 122 | pwselbas 15387 |
. . . . . . . . . . . . . 14
   SubRing ℂfld 
       
          .g mulGrp Poly1 ℂfld   var1 ℂfld        |
124 | 123 | feqmptd 5918 |
. . . . . . . . . . . . 13
   SubRing ℂfld 
       
          .g mulGrp Poly1 ℂfld   var1 ℂfld         .g mulGrp Poly1 ℂfld   var1 ℂfld        |
125 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    SubRing ℂfld

 
     
      ℂfld   |
126 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
    SubRing ℂfld

 
     
        |
127 | 53, 115, 4, 54, 94, 125, 126 | evl1vard 18925 |
. . . . . . . . . . . . . . . . 17
    SubRing ℂfld

 
     
       var1 ℂfld
   Poly1 ℂfld     var1 ℂfld       |
128 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
.g mulGrp ℂfld .g mulGrp ℂfld  |
129 | 114 | adantr 467 |
. . . . . . . . . . . . . . . . 17
    SubRing ℂfld

 
     
        |
130 | 53, 54, 4, 94, 125, 126, 127, 117, 128, 129 | evl1expd 18933 |
. . . . . . . . . . . . . . . 16
    SubRing ℂfld

 
     
         .g mulGrp Poly1 ℂfld   var1 ℂfld    Poly1 ℂfld       .g mulGrp Poly1 ℂfld   var1 ℂfld       .g mulGrp ℂfld      |
131 | 130 | simprd 465 |
. . . . . . . . . . . . . . 15
    SubRing ℂfld

 
     
            .g mulGrp Poly1 ℂfld   var1 ℂfld       .g mulGrp ℂfld     |
132 | | cnfldexp 19001 |
. . . . . . . . . . . . . . . 16
 
   .g mulGrp ℂfld         |
133 | 126, 129,
132 | syl2anc 667 |
. . . . . . . . . . . . . . 15
    SubRing ℂfld

 
     
        .g mulGrp ℂfld         |
134 | 131, 133 | eqtrd 2485 |
. . . . . . . . . . . . . 14
    SubRing ℂfld

 
     
            .g mulGrp Poly1 ℂfld   var1 ℂfld           |
135 | 134 | mpteq2dva 4489 |
. . . . . . . . . . . . 13
   SubRing ℂfld 
       
            .g mulGrp Poly1 ℂfld   var1 ℂfld              |
136 | 124, 135 | eqtrd 2485 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       
          .g mulGrp Poly1 ℂfld   var1 ℂfld          |
137 | 136, 121 | eqeltrrd 2530 |
. . . . . . . . . . 11
   SubRing ℂfld 
       
                 |
138 | 82 | subrgmcl 18020 |
. . . . . . . . . . 11
      SubRing ℂfld s                         
             ℂfld s                 |
139 | 90, 107, 137, 138 | syl3anc 1268 |
. . . . . . . . . 10
   SubRing ℂfld 
       
                  ℂfld s                 |
140 | 89, 139 | eqeltrrd 2530 |
. . . . . . . . 9
   SubRing ℂfld 
       
                       |
141 | 140, 36 | fmptd 6046 |
. . . . . . . 8
  SubRing ℂfld

 
                                      |
142 | 36, 8, 140, 40 | fsuppmptdm 7894 |
. . . . . . . 8
  SubRing ℂfld

 
                        finSupp    ℂfld s     |
143 | 5, 51, 8, 66, 141, 142 | gsumsubmcl 17552 |
. . . . . . 7
  SubRing ℂfld

 
       ℂfld s  g                          |
144 | 47, 143 | eqeltrrd 2530 |
. . . . . 6
  SubRing ℂfld

 
                              |
145 | | eleq1 2517 |
. . . . . 6
                       
                         |
146 | 144, 145 | syl5ibrcom 226 |
. . . . 5
  SubRing ℂfld

 
                        
       |
147 | 146 | rexlimdvva 2886 |
. . . 4
 SubRing ℂfld
                           
       |
148 | 2, 147 | syl5 33 |
. . 3
 SubRing ℂfld
 Poly 
       |
149 | | ffun 5731 |
. . . . . 6
      Poly1 ℂfld      ℂfld s  
  |
150 | 96, 149 | ax-mp 5 |
. . . . 5
 |
151 | | fvelima 5917 |
. . . . 5
       
      |
152 | 150, 151 | mpan 676 |
. . . 4
     
      |
153 | 100 | sselda 3432 |
. . . . . . . . . . 11
  SubRing ℂfld
    Poly1 ℂfld   |
154 | | eqid 2451 |
. . . . . . . . . . . 12
   Poly1 ℂfld    Poly1 ℂfld  |
155 | | eqid 2451 |
. . . . . . . . . . . 12
coe1  coe1   |
156 | 54, 115, 94, 154, 111, 117, 155 | ply1coe 18889 |
. . . . . . . . . . 11
 ℂfld    Poly1 ℂfld   Poly1 ℂfld g    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      |
157 | 9, 153, 156 | sylancr 669 |
. . . . . . . . . 10
  SubRing ℂfld
  Poly1 ℂfld
g    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      |
158 | 157 | fveq2d 5869 |
. . . . . . . . 9
  SubRing ℂfld
         Poly1 ℂfld g    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld       |
159 | | eqid 2451 |
. . . . . . . . . 10
   Poly1 ℂfld    Poly1 ℂfld  |
160 | 54 | ply1ring 18841 |
. . . . . . . . . . . 12
ℂfld Poly1 ℂfld   |
161 | 9, 160 | ax-mp 5 |
. . . . . . . . . . 11
Poly1 ℂfld
 |
162 | | ringcmn 17811 |
. . . . . . . . . . 11
 Poly1 ℂfld
Poly1 ℂfld
CMnd |
163 | 161, 162 | mp1i 13 |
. . . . . . . . . 10
  SubRing ℂfld
 Poly1 ℂfld CMnd |
164 | | ringmnd 17789 |
. . . . . . . . . . 11
 ℂfld s 
ℂfld s    |
165 | 49, 164 | mp1i 13 |
. . . . . . . . . 10
  SubRing ℂfld
 ℂfld s    |
166 | | nn0ex 10875 |
. . . . . . . . . . 11
 |
167 | 166 | a1i 11 |
. . . . . . . . . 10
  SubRing ℂfld
   |
168 | | rhmghm 17953 |
. . . . . . . . . . . 12
  Poly1 ℂfld
RingHom ℂfld s  
 Poly1 ℂfld ℂfld s     |
169 | 56, 168 | ax-mp 5 |
. . . . . . . . . . 11
 Poly1 ℂfld ℂfld s    |
170 | | ghmmhm 16893 |
. . . . . . . . . . 11
  Poly1 ℂfld
ℂfld s  
 Poly1 ℂfld MndHom ℂfld s     |
171 | 169, 170 | mp1i 13 |
. . . . . . . . . 10
  SubRing ℂfld
  Poly1 ℂfld MndHom ℂfld s     |
172 | 54 | ply1lmod 18845 |
. . . . . . . . . . . . 13
ℂfld Poly1 ℂfld   |
173 | 9, 172 | mp1i 13 |
. . . . . . . . . . . 12
   SubRing ℂfld 

Poly1 ℂfld
  |
174 | 12 | ad2antrr 732 |
. . . . . . . . . . . . 13
   SubRing ℂfld 

  |
175 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
         |
176 | 155, 59, 58, 175 | coe1f 18804 |
. . . . . . . . . . . . . . . 16
 coe1            |
177 | 57 | subrgbas 18017 |
. . . . . . . . . . . . . . . . 17
 SubRing ℂfld
      |
178 | 177 | feq3d 5716 |
. . . . . . . . . . . . . . . 16
 SubRing ℂfld
 coe1      coe1             |
179 | 176, 178 | syl5ibr 225 |
. . . . . . . . . . . . . . 15
 SubRing ℂfld
 coe1         |
180 | 179 | imp 431 |
. . . . . . . . . . . . . 14
  SubRing ℂfld
 coe1        |
181 | 180 | ffvelrnda 6022 |
. . . . . . . . . . . . 13
   SubRing ℂfld 

 coe1       |
182 | 174, 181 | sseldd 3433 |
. . . . . . . . . . . 12
   SubRing ℂfld 

 coe1       |
183 | 111 | ringmgp 17786 |
. . . . . . . . . . . . . 14
 Poly1 ℂfld
mulGrp Poly1 ℂfld   |
184 | 161, 183 | mp1i 13 |
. . . . . . . . . . . . 13
   SubRing ℂfld 

mulGrp Poly1 ℂfld   |
185 | | simpr 463 |
. . . . . . . . . . . . 13
   SubRing ℂfld 

  |
186 | 115, 54, 94 | vr1cl 18810 |
. . . . . . . . . . . . . 14
ℂfld var1 ℂfld    Poly1 ℂfld   |
187 | 9, 186 | mp1i 13 |
. . . . . . . . . . . . 13
   SubRing ℂfld 

var1 ℂfld
   Poly1 ℂfld   |
188 | 111, 94 | mgpbas 17729 |
. . . . . . . . . . . . . 14
   Poly1 ℂfld    mulGrp Poly1 ℂfld   |
189 | 188, 117 | mulgnn0cl 16774 |
. . . . . . . . . . . . 13
  mulGrp Poly1 ℂfld var1 ℂfld
   Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld    Poly1 ℂfld   |
190 | 184, 185,
187, 189 | syl3anc 1268 |
. . . . . . . . . . . 12
   SubRing ℂfld 

  .g mulGrp Poly1 ℂfld   var1 ℂfld    Poly1 ℂfld   |
191 | 54 | ply1sca 18846 |
. . . . . . . . . . . . . 14
ℂfld ℂfld Scalar Poly1 ℂfld   |
192 | 9, 191 | ax-mp 5 |
. . . . . . . . . . . . 13
ℂfld
Scalar Poly1 ℂfld  |
193 | 94, 192, 154, 4 | lmodvscl 18108 |
. . . . . . . . . . . 12
  Poly1 ℂfld  coe1       .g mulGrp Poly1 ℂfld   var1 ℂfld    Poly1 ℂfld    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld     Poly1 ℂfld   |
194 | 173, 182,
190, 193 | syl3anc 1268 |
. . . . . . . . . . 11
   SubRing ℂfld 

  coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld     Poly1 ℂfld   |
195 | | eqid 2451 |
. . . . . . . . . . 11

  coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld    |
196 | 194, 195 | fmptd 6046 |
. . . . . . . . . 10
  SubRing ℂfld
    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld          Poly1 ℂfld   |
197 | 166 | mptex 6136 |
. . . . . . . . . . . . 13

  coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld    |
198 | | funmpt 5618 |
. . . . . . . . . . . . 13
   coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld    |
199 | | fvex 5875 |
. . . . . . . . . . . . 13
   Poly1 ℂfld  |
200 | 197, 198,
199 | 3pm3.2i 1186 |
. . . . . . . . . . . 12
    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      Poly1 ℂfld   |
201 | 200 | a1i 11 |
. . . . . . . . . . 11
  SubRing ℂfld
     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld  

  coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      Poly1 ℂfld    |
202 | 155, 94, 54, 17 | coe1sfi 18806 |
. . . . . . . . . . . . 13
    Poly1 ℂfld
coe1  finSupp   |
203 | 153, 202 | syl 17 |
. . . . . . . . . . . 12
  SubRing ℂfld
 coe1 
finSupp   |
204 | 203 | fsuppimpd 7890 |
. . . . . . . . . . 11
  SubRing ℂfld
  coe1  supp    |
205 | 180 | feqmptd 5918 |
. . . . . . . . . . . . . 14
  SubRing ℂfld
 coe1    coe1        |
206 | 205 | oveq1d 6305 |
. . . . . . . . . . . . 13
  SubRing ℂfld
  coe1  supp     coe1      supp    |
207 | | eqimss2 3485 |
. . . . . . . . . . . . 13
  coe1  supp     coe1      supp   
 coe1      supp   coe1  supp    |
208 | 206, 207 | syl 17 |
. . . . . . . . . . . 12
  SubRing ℂfld
    coe1      supp 
 coe1  supp
   |
209 | 9, 172 | mp1i 13 |
. . . . . . . . . . . . 13
  SubRing ℂfld
 Poly1 ℂfld   |
210 | 94, 192, 154, 17, 159 | lmod0vs 18124 |
. . . . . . . . . . . . 13
  Poly1 ℂfld    Poly1 ℂfld       Poly1 ℂfld      Poly1 ℂfld   |
211 | 209, 210 | sylan 474 |
. . . . . . . . . . . 12
   SubRing ℂfld 
   Poly1 ℂfld       Poly1 ℂfld      Poly1 ℂfld   |
212 | | c0ex 9637 |
. . . . . . . . . . . . 13
 |
213 | 212 | a1i 11 |
. . . . . . . . . . . 12
  SubRing ℂfld
   |
214 | 208, 211,
181, 190, 213 | suppssov1 6947 |
. . . . . . . . . . 11
  SubRing ℂfld
     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld   supp    Poly1 ℂfld   coe1  supp    |
215 | | suppssfifsupp 7898 |
. . . . . . . . . . 11
      coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      Poly1 ℂfld    coe1  supp      coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld   supp    Poly1 ℂfld   coe1  supp       coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld   finSupp    Poly1 ℂfld   |
216 | 201, 204,
214, 215 | syl12anc 1266 |
. . . . . . . . . 10
  SubRing ℂfld
    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld   finSupp    Poly1 ℂfld   |
217 | 94, 159, 163, 165, 167, 171, 196, 216 | gsummhm 17571 |
. . . . . . . . 9
  SubRing ℂfld
  ℂfld s 
g     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld         Poly1 ℂfld g    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld       |
218 | | eqidd 2452 |
. . . . . . . . . . . 12
  SubRing ℂfld
    coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld     |
219 | 96 | a1i 11 |
. . . . . . . . . . . . 13
  SubRing ℂfld
      Poly1 ℂfld      ℂfld s     |
220 | 219 | feqmptd 5918 |
. . . . . . . . . . . 12
  SubRing ℂfld
     Poly1 ℂfld        |
221 | | fveq2 5865 |
. . . . . . . . . . . 12
   coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld           coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld     |
222 | 194, 218,
220, 221 | fmptco 6056 |
. . . . . . . . . . 11
  SubRing ℂfld
 
   coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld    
     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      |
223 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
   SubRing ℂfld 

ℂfld   |
224 | 6 | a1i 11 |
. . . . . . . . . . . . . . 15
   SubRing ℂfld 

  |
225 | 96 | ffvelrni 6021 |
. . . . . . . . . . . . . . . 16
   coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld     Poly1 ℂfld
     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      ℂfld s     |
226 | 194, 225 | syl 17 |
. . . . . . . . . . . . . . 15
   SubRing ℂfld 

     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      ℂfld s     |
227 | 3, 4, 67, 223, 224, 226 | pwselbas 15387 |
. . . . . . . . . . . . . 14
   SubRing ℂfld 

     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld         |
228 | 227 | feqmptd 5918 |
. . . . . . . . . . . . 13
   SubRing ℂfld 

     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld          coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld         |
229 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
    SubRing ℂfld
  
ℂfld   |
230 | | simpr 463 |
. . . . . . . . . . . . . . . 16
    SubRing ℂfld
     |
231 | 53, 115, 4, 54, 94, 229, 230 | evl1vard 18925 |
. . . . . . . . . . . . . . . . . 18
    SubRing ℂfld
    var1 ℂfld    Poly1 ℂfld     var1 ℂfld       |
232 | 185 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
    SubRing ℂfld
     |
233 | 53, 54, 4, 94, 229, 230, 231, 117, 128, 232 | evl1expd 18933 |
. . . . . . . . . . . . . . . . 17
    SubRing ℂfld
      .g mulGrp Poly1 ℂfld   var1 ℂfld    Poly1 ℂfld       .g mulGrp Poly1 ℂfld   var1 ℂfld       .g mulGrp ℂfld      |
234 | 230, 232,
132 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
    SubRing ℂfld
     .g mulGrp ℂfld         |
235 | 234 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . 18
    SubRing ℂfld
          .g mulGrp Poly1 ℂfld   var1 ℂfld       .g mulGrp ℂfld         .g mulGrp Poly1 ℂfld   var1 ℂfld            |
236 | 235 | anbi2d 710 |
. . . . . . . . . . . . . . . . 17
    SubRing ℂfld
       .g mulGrp Poly1 ℂfld   var1 ℂfld    Poly1 ℂfld       .g mulGrp Poly1 ℂfld   var1 ℂfld       .g mulGrp ℂfld       .g mulGrp Poly1 ℂfld   var1 ℂfld    Poly1 ℂfld       .g mulGrp Poly1 ℂfld   var1 ℂfld             |
237 | 233, 236 | mpbid 214 |
. . . . . . . . . . . . . . . 16
    SubRing ℂfld
      .g mulGrp Poly1 ℂfld   var1 ℂfld    Poly1 ℂfld       .g mulGrp Poly1 ℂfld   var1 ℂfld            |
238 | 182 | adantr 467 |
. . . . . . . . . . . . . . . 16
    SubRing ℂfld
    coe1       |
239 | 53, 54, 4, 94, 229, 230, 237, 238, 154, 81 | evl1vsd 18932 |
. . . . . . . . . . . . . . 15
    SubRing ℂfld
      coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld     Poly1 ℂfld       coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld        coe1             |
240 | 239 | simprd 465 |
. . . . . . . . . . . . . 14
    SubRing ℂfld
         coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld        coe1            |
241 | 240 | mpteq2dva 4489 |
. . . . . . . . . . . . 13
   SubRing ℂfld 

       coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld          coe1             |
242 | 228, 241 | eqtrd 2485 |
. . . . . . . . . . . 12
   SubRing ℂfld 

     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      coe1             |
243 | 242 | mpteq2dva 4489 |
. . . . . . . . . . 11
  SubRing ℂfld
       coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld    
   coe1              |
244 | 222, 243 | eqtrd 2485 |
. . . . . . . . . 10
  SubRing ℂfld
 
   coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld    
   coe1              |
245 | 244 | oveq2d 6306 |
. . . . . . . . 9
  SubRing ℂfld
  ℂfld s 
g     coe1         Poly1 ℂfld    .g mulGrp Poly1 ℂfld   var1 ℂfld      ℂfld s  g     coe1               |
246 | 158, 217,
245 | 3eqtr2d 2491 |
. . . . . . . 8
  SubRing ℂfld
      ℂfld s  g     coe1               |
247 | 6 | a1i 11 |
. . . . . . . . 9
  SubRing ℂfld
   |
248 | 9, 10 | mp1i 13 |
. . . . . . . . 9
  SubRing ℂfld

ℂfld CMnd |
249 | 182 | adantlr 721 |
. . . . . . . . . . 11
    SubRing ℂfld
    coe1       |
250 | 33 | adantll 720 |
. . . . . . . . . . 11
    SubRing ℂfld
         |
251 | 249, 250 | mulcld 9663 |
. . . . . . . . . 10
    SubRing ℂfld
     coe1            |
252 | 251 | anasss 653 |
. . . . . . . . 9
   SubRing ℂfld 
     coe1            |
253 | 166 | mptex 6136 |
. . . . . . . . . . . 12

   coe1             |
254 | | funmpt 5618 |
. . . . . . . . . . . 12
    coe1             |
255 | 253, 254,
39 | 3pm3.2i 1186 |
. . . . . . . . . . 11
     coe1           

   coe1               ℂfld s     |
256 | 255 | a1i 11 |
. . . . . . . . . 10
  SubRing ℂfld
      coe1                coe1               ℂfld s      |
257 | | fzfid 12186 |
. . . . . . . . . 10
  SubRing ℂfld
       deg1 ℂfld     deg1 ℂfld        |
258 | | eldifn 3556 |
. . . . . . . . . . . . . . . . . 18
        deg1 ℂfld     deg1 ℂfld      
      deg1 ℂfld     deg1 ℂfld        |
259 | 258 | adantl 468 |
. . . . . . . . . . . . . . . . 17
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld       
      deg1 ℂfld     deg1 ℂfld        |
260 | 153 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld           Poly1 ℂfld   |
261 | | eldifi 3555 |
. . . . . . . . . . . . . . . . . . . . . . 23
        deg1 ℂfld     deg1 ℂfld      
  |
262 | 261 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          |
263 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
deg1 ℂfld
deg1 ℂfld |
264 | 263, 54, 94, 17, 155 | deg1ge 23047 |
. . . . . . . . . . . . . . . . . . . . . . 23
     Poly1 ℂfld  coe1       deg1 ℂfld     |
265 | 264 | 3expia 1210 |
. . . . . . . . . . . . . . . . . . . . . 22
     Poly1 ℂfld    coe1    
 deg1 ℂfld      |
266 | 260, 262,
265 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . 21
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          coe1    
 deg1 ℂfld      |
267 | | 0xr 9687 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
268 | 263, 54, 94 | deg1xrcl 23031 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    Poly1 ℂfld
 deg1 ℂfld     |
269 | 153, 268 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  SubRing ℂfld
  deg1 ℂfld     |
270 | 269 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld         deg1 ℂfld     |
271 | | xrmax2 11471 |
. . . . . . . . . . . . . . . . . . . . . . 23
   deg1 ℂfld     deg1 ℂfld      deg1 ℂfld     deg1 ℂfld       |
272 | 267, 270,
271 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . 22
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld         deg1 ℂfld      deg1 ℂfld     deg1 ℂfld       |
273 | 262 | nn0red 10926 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          |
274 | 273 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . . . . . 23
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          |
275 | | ifcl 3923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
deg1 ℂfld  
    deg1 ℂfld     deg1 ℂfld       |
276 | 270, 267,
275 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . . . 23
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld           deg1 ℂfld     deg1 ℂfld       |
277 | | xrletr 11455 |
. . . . . . . . . . . . . . . . . . . . . . 23
   deg1 ℂfld  
 
 deg1 ℂfld     deg1 ℂfld         deg1 ℂfld    deg1 ℂfld      deg1 ℂfld     deg1 ℂfld         deg1 ℂfld     deg1 ℂfld        |
278 | 274, 270,
276, 277 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . 22
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld           deg1 ℂfld    deg1 ℂfld      deg1 ℂfld     deg1 ℂfld         deg1 ℂfld     deg1 ℂfld        |
279 | 272, 278 | mpan2d 680 |
. . . . . . . . . . . . . . . . . . . . 21
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld        
 deg1 ℂfld     
deg1 ℂfld     deg1 ℂfld        |
280 | 266, 279 | syld 45 |
. . . . . . . . . . . . . . . . . . . 20
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          coe1    
 
 deg1 ℂfld     deg1 ℂfld        |
281 | 280, 262 | jctild 546 |
. . . . . . . . . . . . . . . . . . 19
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          coe1     
 
 deg1 ℂfld     deg1 ℂfld         |
282 | 263, 54, 94 | deg1cl 23032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    Poly1 ℂfld
 deg1 ℂfld        |
283 | 153, 282 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
  SubRing ℂfld
  deg1 ℂfld        |
284 | | elun 3574 |
. . . . . . . . . . . . . . . . . . . . . . 23
  deg1 ℂfld     
  deg1 ℂfld  
 deg1 ℂfld       |
285 | 283, 284 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . 22
  SubRing ℂfld
  
deg1 ℂfld  
 deg1 ℂfld       |
286 | | nn0ge0 10895 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  deg1 ℂfld  

deg1 ℂfld     |
287 | 286 | iftrued 3889 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  deg1 ℂfld  
 
 deg1 ℂfld     deg1 ℂfld     
deg1 ℂfld     |
288 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  deg1 ℂfld  
 deg1 ℂfld     |
289 | 287, 288 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . 23
  deg1 ℂfld  
 
 deg1 ℂfld     deg1 ℂfld       |
290 | | mnflt0 11427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
291 | | mnfxr 11414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
292 | | xrltnle 9701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
293 | 291, 267,
292 | mp2an 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  |
294 | 290, 293 | mpbi 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
295 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  deg1 ℂfld    
deg1 ℂfld     |
296 | 295 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  deg1 ℂfld      deg1 ℂfld  
   |
297 | 294, 296 | mtbiri 305 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  deg1 ℂfld     deg1 ℂfld     |
298 | 297 | iffalsed 3892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  deg1 ℂfld      
deg1 ℂfld     deg1 ℂfld       |
299 | | 0nn0 10884 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
300 | 298, 299 | syl6eqel 2537 |
. . . . . . . . . . . . . . . . . . . . . . 23
  deg1 ℂfld      
deg1 ℂfld     deg1 ℂfld       |
301 | 289, 300 | jaoi 381 |
. . . . . . . . . . . . . . . . . . . . . 22
  
deg1 ℂfld  
 deg1 ℂfld    
 
 deg1 ℂfld     deg1 ℂfld       |
302 | 285, 301 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
  SubRing ℂfld
    deg1 ℂfld     deg1 ℂfld       |
303 | 302 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . 20
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld           deg1 ℂfld     deg1 ℂfld       |
304 | | fznn0 11886 |
. . . . . . . . . . . . . . . . . . . 20
    deg1 ℂfld     deg1 ℂfld            deg1 ℂfld     deg1 ℂfld      
 
 deg1 ℂfld     deg1 ℂfld         |
305 | 303, 304 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld               deg1 ℂfld     deg1 ℂfld      
 
 deg1 ℂfld     deg1 ℂfld         |
306 | 281, 305 | sylibrd 238 |
. . . . . . . . . . . . . . . . . 18
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          coe1           deg1 ℂfld     deg1 ℂfld         |
307 | 306 | necon1bd 2642 |
. . . . . . . . . . . . . . . . 17
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld        
      deg1 ℂfld     deg1 ℂfld       coe1        |
308 | 259, 307 | mpd 15 |
. . . . . . . . . . . . . . . 16
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld         coe1       |
309 | 308 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          coe1                  |
310 | 261, 250 | sylan2 477 |
. . . . . . . . . . . . . . . 16
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld              |
311 | 310 | mul02d 9831 |
. . . . . . . . . . . . . . 15
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld                |
312 | 309, 311 | eqtrd 2485 |
. . . . . . . . . . . . . 14
    SubRing ℂfld
         deg1 ℂfld     deg1 ℂfld          coe1            |
313 | 312 | an32s 813 |
. . . . . . . . . . . . 13
    SubRing ℂfld
        deg1 ℂfld     deg1 ℂfld           coe1            |
314 | 313 | mpteq2dva 4489 |
. . . . . . . . . . . 12
   SubRing ℂfld 
       deg1 ℂfld     deg1 ℂfld           coe1               |
315 | | fconstmpt 4878 |
. . . . . . . . . . . . 13
       |
316 | | ringmnd 17789 |
. . . . . . . . . . . . . . 15
ℂfld ℂfld   |
317 | 9, 316 | ax-mp 5 |
. . . . . . . . . . . . . 14
ℂfld  |
318 | 3, 17 | pws0g 16572 |
. . . . . . . . . . . . . 14
 ℂfld

       ℂfld s     |
319 | 317, 6, 318 | mp2an 678 |
. . . . . . . . . . . . 13
       ℂfld s    |
320 | 315, 319 | eqtr3i 2475 |
. . . . . . . . . . . 12
     ℂfld s    |
321 | 314, 320 | syl6eq 2501 |
. . . . . . . . . . 11
   SubRing ℂfld 
       deg1 ℂfld     deg1 ℂfld           coe1              ℂfld s     |
322 | 321, 167 | suppss2 6949 |
. . . . . . . . . 10
  SubRing ℂfld
      coe1            supp    ℂfld s          deg1 ℂfld     deg1 ℂfld        |
323 | | suppssfifsupp 7898 |
. . . . . . . . . 10
       coe1                coe1               ℂfld s           deg1 ℂfld     deg1 ℂfld           coe1            supp    ℂfld s          deg1 ℂfld     deg1 ℂfld            coe1            finSupp    ℂfld s     |
324 | 256, 257,
322, 323 | syl12anc 1266 |
. . . . . . . . 9
  SubRing ℂfld
     coe1            finSupp    ℂfld s     |
325 | 3, 4, 5, 247, 167, 248, 252, 324 | pwsgsum 17611 |
. . . . . . . 8
  SubRing ℂfld
  ℂfld s 
g     coe1              ℂfld g    coe1               |
326 | | elfznn0 11887 |
. . . . . . . . . . . . 13
      
deg1 ℂfld     deg1 ℂfld        |
327 | 326 | ssriv 3436 |
. . . . . . . . . . . 12
      deg1 ℂfld     deg1 ℂfld       |
328 | | resmpt 5154 |
. . . . . . . . . . . 12
     
 deg1 ℂfld     deg1 ℂfld     
    coe1                 deg1 ℂfld     deg1 ℂfld             
deg1 ℂfld     deg1 ℂfld        coe1             |
329 | 327, 328 | ax-mp 5 |
. . . . . . . . . . 11
    coe1                 deg1 ℂfld     deg1 ℂfld             
deg1 ℂfld     deg1 ℂfld        coe1            |
330 | 329 | oveq2i 6301 |
. . . . . . . . . 10
ℂfld g     coe1          
      deg1 ℂfld     deg1 ℂfld        ℂfld g       
deg1 ℂfld     deg1 ℂfld        coe1             |
331 | 9, 10 | mp1i 13 |
. . . . . . . . . . 11
   SubRing ℂfld 

ℂfld CMnd |
332 | 166 | a1i 11 |
. . . . . . . . . . 11
    |