Metamath Proof Explorer

Theorem plypf1

Description: Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015) (Proof shortened by AV, 29-Sep-2019)

Ref Expression
Hypotheses plypf1.r 
|- R = ( CCfld |`s S )
plypf1.p 
|- P = ( Poly1 ` R )
plypf1.a 
|- A = ( Base ` P )
plypf1.e 
|- E = ( eval1 ` CCfld )
Assertion plypf1 
|- ( S e. ( SubRing ` CCfld ) -> ( Poly ` S ) = ( E " A ) )

Proof

Step Hyp Ref Expression
1 plypf1.r 
 |-  R = ( CCfld |`s S )
2 plypf1.p 
 |-  P = ( Poly1 ` R )
3 plypf1.a 
 |-  A = ( Base ` P )
4 plypf1.e 
 |-  E = ( eval1 ` CCfld )
5 elply 
 |-  ( f e. ( Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
6 5 simprbi 
 |-  ( f e. ( Poly ` S ) -> E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
7 eqid 
 |-  ( CCfld ^s CC ) = ( CCfld ^s CC )
8 cnfldbas 
 |-  CC = ( Base ` CCfld )
9 eqid 
 |-  ( 0g ` ( CCfld ^s CC ) ) = ( 0g ` ( CCfld ^s CC ) )
10 cnex 
 |-  CC e. _V
11 10 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> CC e. _V )
12 fzfid 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0 ... n ) e. Fin )
13 cnring 
 |-  CCfld e. Ring
14 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
15 13 14 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> CCfld e. CMnd )
16 8 subrgss 
 |-  ( S e. ( SubRing ` CCfld ) -> S C_ CC )
17 16 ad2antrr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> S C_ CC )
18 elmapi 
 |-  ( a e. ( ( S u. { 0 } ) ^m NN0 ) -> a : NN0 --> ( S u. { 0 } ) )
19 18 ad2antll 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> ( S u. { 0 } ) )
20 subrgsubg 
 |-  ( S e. ( SubRing ` CCfld ) -> S e. ( SubGrp ` CCfld ) )
21 cnfld0 
 |-  0 = ( 0g ` CCfld )
22 21 subg0cl 
 |-  ( S e. ( SubGrp ` CCfld ) -> 0 e. S )
23 20 22 syl 
 |-  ( S e. ( SubRing ` CCfld ) -> 0 e. S )
24 23 adantr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> 0 e. S )
25 24 snssd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> { 0 } C_ S )
26 ssequn2 
 |-  ( { 0 } C_ S <-> ( S u. { 0 } ) = S )
27 25 26 sylib 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( S u. { 0 } ) = S )
28 27 feq3d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( a : NN0 --> ( S u. { 0 } ) <-> a : NN0 --> S ) )
29 19 28 mpbid 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> a : NN0 --> S )
30 elfznn0 
 |-  ( k e. ( 0 ... n ) -> k e. NN0 )
31 ffvelcdm 
 |-  ( ( a : NN0 --> S /\ k e. NN0 ) -> ( a ` k ) e. S )
32 29 30 31 syl2an 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( a ` k ) e. S )
33 17 32 sseldd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( a ` k ) e. CC )
34 33 adantrl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> ( a ` k ) e. CC )
35 simprl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> z e. CC )
36 30 ad2antll 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> k e. NN0 )
37 expcl 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
38 35 36 37 syl2anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> ( z ^ k ) e. CC )
39 34 38 mulcld 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ ( z e. CC /\ k e. ( 0 ... n ) ) ) -> ( ( a ` k ) x. ( z ^ k ) ) e. CC )
40 eqid 
 |-  ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) = ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) )
41 10 mptex 
 |-  ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) e. _V
42 41 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) e. _V )
43 fvex 
 |-  ( 0g ` ( CCfld ^s CC ) ) e. _V
44 43 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( 0g ` ( CCfld ^s CC ) ) e. _V )
45 40 12 42 44 fsuppmptdm 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) finSupp ( 0g ` ( CCfld ^s CC ) ) )
46 7 8 9 11 12 15 39 45 pwsgsum 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( ( CCfld ^s CC ) gsum ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> ( CCfld gsum ( k e. ( 0 ... n ) |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
47 fzfid 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> ( 0 ... n ) e. Fin )
48 39 anassrs 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) /\ k e. ( 0 ... n ) ) -> ( ( a ` k ) x. ( z ^ k ) ) e. CC )
49 47 48 gsumfsum 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ z e. CC ) -> ( CCfld gsum ( k e. ( 0 ... n ) |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) = sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) )
50 49 mpteq2dva 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( z e. CC |-> ( CCfld gsum ( k e. ( 0 ... n ) |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
51 46 50 eqtrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( ( CCfld ^s CC ) gsum ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
52 7 pwsring 
 |-  ( ( CCfld e. Ring /\ CC e. _V ) -> ( CCfld ^s CC ) e. Ring )
53 13 10 52 mp2an 
 |-  ( CCfld ^s CC ) e. Ring
54 ringcmn 
 |-  ( ( CCfld ^s CC ) e. Ring -> ( CCfld ^s CC ) e. CMnd )
55 53 54 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( CCfld ^s CC ) e. CMnd )
56 cncrng 
 |-  CCfld e. CRing
57 eqid 
 |-  ( Poly1 ` CCfld ) = ( Poly1 ` CCfld )
58 4 57 7 8 evl1rhm 
 |-  ( CCfld e. CRing -> E e. ( ( Poly1 ` CCfld ) RingHom ( CCfld ^s CC ) ) )
59 56 58 ax-mp 
 |-  E e. ( ( Poly1 ` CCfld ) RingHom ( CCfld ^s CC ) )
60 57 1 2 3 subrgply1 
 |-  ( S e. ( SubRing ` CCfld ) -> A e. ( SubRing ` ( Poly1 ` CCfld ) ) )
61 60 adantr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> A e. ( SubRing ` ( Poly1 ` CCfld ) ) )
62 rhmima 
 |-  ( ( E e. ( ( Poly1 ` CCfld ) RingHom ( CCfld ^s CC ) ) /\ A e. ( SubRing ` ( Poly1 ` CCfld ) ) ) -> ( E " A ) e. ( SubRing ` ( CCfld ^s CC ) ) )
63 59 61 62 sylancr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. ( SubRing ` ( CCfld ^s CC ) ) )
64 subrgsubg 
 |-  ( ( E " A ) e. ( SubRing ` ( CCfld ^s CC ) ) -> ( E " A ) e. ( SubGrp ` ( CCfld ^s CC ) ) )
65 subgsubm 
 |-  ( ( E " A ) e. ( SubGrp ` ( CCfld ^s CC ) ) -> ( E " A ) e. ( SubMnd ` ( CCfld ^s CC ) ) )
66 63 64 65 3syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( E " A ) e. ( SubMnd ` ( CCfld ^s CC ) ) )
67 eqid 
 |-  ( Base ` ( CCfld ^s CC ) ) = ( Base ` ( CCfld ^s CC ) )
68 13 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> CCfld e. Ring )
69 10 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> CC e. _V )
70 fconst6g 
 |-  ( ( a ` k ) e. CC -> ( CC X. { ( a ` k ) } ) : CC --> CC )
71 33 70 syl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( CC X. { ( a ` k ) } ) : CC --> CC )
72 7 8 67 pwselbasb 
 |-  ( ( CCfld e. Ring /\ CC e. _V ) -> ( ( CC X. { ( a ` k ) } ) e. ( Base ` ( CCfld ^s CC ) ) <-> ( CC X. { ( a ` k ) } ) : CC --> CC ) )
73 13 10 72 mp2an 
 |-  ( ( CC X. { ( a ` k ) } ) e. ( Base ` ( CCfld ^s CC ) ) <-> ( CC X. { ( a ` k ) } ) : CC --> CC )
74 71 73 sylibr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( CC X. { ( a ` k ) } ) e. ( Base ` ( CCfld ^s CC ) ) )
75 38 anass1rs 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( z ^ k ) e. CC )
76 75 fmpttd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( z ^ k ) ) : CC --> CC )
77 7 8 67 pwselbasb 
 |-  ( ( CCfld e. Ring /\ CC e. _V ) -> ( ( z e. CC |-> ( z ^ k ) ) e. ( Base ` ( CCfld ^s CC ) ) <-> ( z e. CC |-> ( z ^ k ) ) : CC --> CC ) )
78 13 10 77 mp2an 
 |-  ( ( z e. CC |-> ( z ^ k ) ) e. ( Base ` ( CCfld ^s CC ) ) <-> ( z e. CC |-> ( z ^ k ) ) : CC --> CC )
79 76 78 sylibr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( z ^ k ) ) e. ( Base ` ( CCfld ^s CC ) ) )
80 cnfldmul 
 |-  x. = ( .r ` CCfld )
81 eqid 
 |-  ( .r ` ( CCfld ^s CC ) ) = ( .r ` ( CCfld ^s CC ) )
82 7 67 68 69 74 79 80 81 pwsmulrval 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( CC X. { ( a ` k ) } ) ( .r ` ( CCfld ^s CC ) ) ( z e. CC |-> ( z ^ k ) ) ) = ( ( CC X. { ( a ` k ) } ) oF x. ( z e. CC |-> ( z ^ k ) ) ) )
83 33 adantr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( a ` k ) e. CC )
84 fconstmpt 
 |-  ( CC X. { ( a ` k ) } ) = ( z e. CC |-> ( a ` k ) )
85 84 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( CC X. { ( a ` k ) } ) = ( z e. CC |-> ( a ` k ) ) )
86 eqidd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( z ^ k ) ) = ( z e. CC |-> ( z ^ k ) ) )
87 69 83 75 85 86 offval2 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( CC X. { ( a ` k ) } ) oF x. ( z e. CC |-> ( z ^ k ) ) ) = ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) )
88 82 87 eqtrd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( CC X. { ( a ` k ) } ) ( .r ` ( CCfld ^s CC ) ) ( z e. CC |-> ( z ^ k ) ) ) = ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) )
89 63 adantr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E " A ) e. ( SubRing ` ( CCfld ^s CC ) ) )
90 eqid 
 |-  ( algSc ` ( Poly1 ` CCfld ) ) = ( algSc ` ( Poly1 ` CCfld ) )
91 4 57 8 90 evl1sca 
 |-  ( ( CCfld e. CRing /\ ( a ` k ) e. CC ) -> ( E ` ( ( algSc ` ( Poly1 ` CCfld ) ) ` ( a ` k ) ) ) = ( CC X. { ( a ` k ) } ) )
92 56 33 91 sylancr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( ( algSc ` ( Poly1 ` CCfld ) ) ` ( a ` k ) ) ) = ( CC X. { ( a ` k ) } ) )
93 eqid 
 |-  ( Base ` ( Poly1 ` CCfld ) ) = ( Base ` ( Poly1 ` CCfld ) )
94 93 67 rhmf 
 |-  ( E e. ( ( Poly1 ` CCfld ) RingHom ( CCfld ^s CC ) ) -> E : ( Base ` ( Poly1 ` CCfld ) ) --> ( Base ` ( CCfld ^s CC ) ) )
95 59 94 ax-mp 
 |-  E : ( Base ` ( Poly1 ` CCfld ) ) --> ( Base ` ( CCfld ^s CC ) )
96 ffn 
 |-  ( E : ( Base ` ( Poly1 ` CCfld ) ) --> ( Base ` ( CCfld ^s CC ) ) -> E Fn ( Base ` ( Poly1 ` CCfld ) ) )
97 95 96 mp1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> E Fn ( Base ` ( Poly1 ` CCfld ) ) )
98 93 subrgss 
 |-  ( A e. ( SubRing ` ( Poly1 ` CCfld ) ) -> A C_ ( Base ` ( Poly1 ` CCfld ) ) )
99 60 98 syl 
 |-  ( S e. ( SubRing ` CCfld ) -> A C_ ( Base ` ( Poly1 ` CCfld ) ) )
100 99 ad2antrr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> A C_ ( Base ` ( Poly1 ` CCfld ) ) )
101 simpll 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> S e. ( SubRing ` CCfld ) )
102 57 90 1 2 101 3 8 33 subrg1asclcl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( ( algSc ` ( Poly1 ` CCfld ) ) ` ( a ` k ) ) e. A <-> ( a ` k ) e. S ) )
103 32 102 mpbird 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( algSc ` ( Poly1 ` CCfld ) ) ` ( a ` k ) ) e. A )
104 fnfvima 
 |-  ( ( E Fn ( Base ` ( Poly1 ` CCfld ) ) /\ A C_ ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( algSc ` ( Poly1 ` CCfld ) ) ` ( a ` k ) ) e. A ) -> ( E ` ( ( algSc ` ( Poly1 ` CCfld ) ) ` ( a ` k ) ) ) e. ( E " A ) )
105 97 100 103 104 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( ( algSc ` ( Poly1 ` CCfld ) ) ` ( a ` k ) ) ) e. ( E " A ) )
106 92 105 eqeltrrd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( CC X. { ( a ` k ) } ) e. ( E " A ) )
107 67 subrgss 
 |-  ( ( E " A ) e. ( SubRing ` ( CCfld ^s CC ) ) -> ( E " A ) C_ ( Base ` ( CCfld ^s CC ) ) )
108 89 107 syl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E " A ) C_ ( Base ` ( CCfld ^s CC ) ) )
109 60 ad2antrr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> A e. ( SubRing ` ( Poly1 ` CCfld ) ) )
110 eqid 
 |-  ( mulGrp ` ( Poly1 ` CCfld ) ) = ( mulGrp ` ( Poly1 ` CCfld ) )
111 110 subrgsubm 
 |-  ( A e. ( SubRing ` ( Poly1 ` CCfld ) ) -> A e. ( SubMnd ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) )
112 109 111 syl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> A e. ( SubMnd ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) )
113 30 adantl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> k e. NN0 )
114 eqid 
 |-  ( var1 ` CCfld ) = ( var1 ` CCfld )
115 114 101 1 2 3 subrgvr1cl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( var1 ` CCfld ) e. A )
116 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) )
117 116 submmulgcl 
 |-  ( ( A e. ( SubMnd ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) /\ k e. NN0 /\ ( var1 ` CCfld ) e. A ) -> ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. A )
118 112 113 115 117 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. A )
119 fnfvima 
 |-  ( ( E Fn ( Base ` ( Poly1 ` CCfld ) ) /\ A C_ ( Base ` ( Poly1 ` CCfld ) ) /\ ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. A ) -> ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) e. ( E " A ) )
120 97 100 118 119 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) e. ( E " A ) )
121 108 120 sseldd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) e. ( Base ` ( CCfld ^s CC ) ) )
122 7 8 67 68 69 121 pwselbas 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) : CC --> CC )
123 122 feqmptd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) = ( z e. CC |-> ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) ) )
124 56 a1i 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> CCfld e. CRing )
125 simpr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> z e. CC )
126 4 114 8 57 93 124 125 evl1vard 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( ( var1 ` CCfld ) e. ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( E ` ( var1 ` CCfld ) ) ` z ) = z ) )
127 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
128 113 adantr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> k e. NN0 )
129 4 57 8 93 124 125 126 116 127 128 evl1expd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( k ( .g ` ( mulGrp ` CCfld ) ) z ) ) )
130 129 simprd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( k ( .g ` ( mulGrp ` CCfld ) ) z ) )
131 cnfldexp 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( k ( .g ` ( mulGrp ` CCfld ) ) z ) = ( z ^ k ) )
132 125 128 131 syl2anc 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( k ( .g ` ( mulGrp ` CCfld ) ) z ) = ( z ^ k ) )
133 130 132 eqtrd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) /\ z e. CC ) -> ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( z ^ k ) )
134 133 mpteq2dva 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) ) = ( z e. CC |-> ( z ^ k ) ) )
135 123 134 eqtrd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) = ( z e. CC |-> ( z ^ k ) ) )
136 135 120 eqeltrrd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( z ^ k ) ) e. ( E " A ) )
137 81 subrgmcl 
 |-  ( ( ( E " A ) e. ( SubRing ` ( CCfld ^s CC ) ) /\ ( CC X. { ( a ` k ) } ) e. ( E " A ) /\ ( z e. CC |-> ( z ^ k ) ) e. ( E " A ) ) -> ( ( CC X. { ( a ` k ) } ) ( .r ` ( CCfld ^s CC ) ) ( z e. CC |-> ( z ^ k ) ) ) e. ( E " A ) )
138 89 106 136 137 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( CC X. { ( a ` k ) } ) ( .r ` ( CCfld ^s CC ) ) ( z e. CC |-> ( z ^ k ) ) ) e. ( E " A ) )
139 88 138 eqeltrrd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) /\ k e. ( 0 ... n ) ) -> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) e. ( E " A ) )
140 139 fmpttd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) : ( 0 ... n ) --> ( E " A ) )
141 40 12 139 44 fsuppmptdm 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) finSupp ( 0g ` ( CCfld ^s CC ) ) )
142 9 55 12 66 140 141 gsumsubmcl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( ( CCfld ^s CC ) gsum ( k e. ( 0 ... n ) |-> ( z e. CC |-> ( ( a ` k ) x. ( z ^ k ) ) ) ) ) e. ( E " A ) )
143 51 142 eqeltrrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) e. ( E " A ) )
144 eleq1 
 |-  ( f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> ( f e. ( E " A ) <-> ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) e. ( E " A ) ) )
145 143 144 syl5ibrcom 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( n e. NN0 /\ a e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> f e. ( E " A ) ) )
146 145 rexlimdvva 
 |-  ( S e. ( SubRing ` CCfld ) -> ( E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> f e. ( E " A ) ) )
147 6 146 syl5 
 |-  ( S e. ( SubRing ` CCfld ) -> ( f e. ( Poly ` S ) -> f e. ( E " A ) ) )
148 ffun 
 |-  ( E : ( Base ` ( Poly1 ` CCfld ) ) --> ( Base ` ( CCfld ^s CC ) ) -> Fun E )
149 95 148 ax-mp 
 |-  Fun E
150 fvelima 
 |-  ( ( Fun E /\ f e. ( E " A ) ) -> E. a e. A ( E ` a ) = f )
151 149 150 mpan 
 |-  ( f e. ( E " A ) -> E. a e. A ( E ` a ) = f )
152 99 sselda 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> a e. ( Base ` ( Poly1 ` CCfld ) ) )
153 eqid 
 |-  ( .s ` ( Poly1 ` CCfld ) ) = ( .s ` ( Poly1 ` CCfld ) )
154 eqid 
 |-  ( coe1 ` a ) = ( coe1 ` a )
155 57 114 93 153 110 116 154 ply1coe 
 |-  ( ( CCfld e. Ring /\ a e. ( Base ` ( Poly1 ` CCfld ) ) ) -> a = ( ( Poly1 ` CCfld ) gsum ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) )
156 13 152 155 sylancr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> a = ( ( Poly1 ` CCfld ) gsum ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) )
157 156 fveq2d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( E ` a ) = ( E ` ( ( Poly1 ` CCfld ) gsum ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) ) )
158 eqid 
 |-  ( 0g ` ( Poly1 ` CCfld ) ) = ( 0g ` ( Poly1 ` CCfld ) )
159 57 ply1ring 
 |-  ( CCfld e. Ring -> ( Poly1 ` CCfld ) e. Ring )
160 13 159 ax-mp 
 |-  ( Poly1 ` CCfld ) e. Ring
161 ringcmn 
 |-  ( ( Poly1 ` CCfld ) e. Ring -> ( Poly1 ` CCfld ) e. CMnd )
162 160 161 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( Poly1 ` CCfld ) e. CMnd )
163 ringmnd 
 |-  ( ( CCfld ^s CC ) e. Ring -> ( CCfld ^s CC ) e. Mnd )
164 53 163 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( CCfld ^s CC ) e. Mnd )
165 nn0ex 
 |-  NN0 e. _V
166 165 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> NN0 e. _V )
167 rhmghm 
 |-  ( E e. ( ( Poly1 ` CCfld ) RingHom ( CCfld ^s CC ) ) -> E e. ( ( Poly1 ` CCfld ) GrpHom ( CCfld ^s CC ) ) )
168 59 167 ax-mp 
 |-  E e. ( ( Poly1 ` CCfld ) GrpHom ( CCfld ^s CC ) )
169 ghmmhm 
 |-  ( E e. ( ( Poly1 ` CCfld ) GrpHom ( CCfld ^s CC ) ) -> E e. ( ( Poly1 ` CCfld ) MndHom ( CCfld ^s CC ) ) )
170 168 169 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> E e. ( ( Poly1 ` CCfld ) MndHom ( CCfld ^s CC ) ) )
171 57 ply1lmod 
 |-  ( CCfld e. Ring -> ( Poly1 ` CCfld ) e. LMod )
172 13 171 mp1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( Poly1 ` CCfld ) e. LMod )
173 16 ad2antrr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> S C_ CC )
174 eqid 
 |-  ( Base ` R ) = ( Base ` R )
175 154 3 2 174 coe1f 
 |-  ( a e. A -> ( coe1 ` a ) : NN0 --> ( Base ` R ) )
176 1 subrgbas 
 |-  ( S e. ( SubRing ` CCfld ) -> S = ( Base ` R ) )
177 176 feq3d 
 |-  ( S e. ( SubRing ` CCfld ) -> ( ( coe1 ` a ) : NN0 --> S <-> ( coe1 ` a ) : NN0 --> ( Base ` R ) ) )
178 175 177 imbitrrid 
 |-  ( S e. ( SubRing ` CCfld ) -> ( a e. A -> ( coe1 ` a ) : NN0 --> S ) )
179 178 imp 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( coe1 ` a ) : NN0 --> S )
180 179 ffvelcdmda 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( ( coe1 ` a ) ` k ) e. S )
181 173 180 sseldd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( ( coe1 ` a ) ` k ) e. CC )
182 110 93 mgpbas 
 |-  ( Base ` ( Poly1 ` CCfld ) ) = ( Base ` ( mulGrp ` ( Poly1 ` CCfld ) ) )
183 110 ringmgp 
 |-  ( ( Poly1 ` CCfld ) e. Ring -> ( mulGrp ` ( Poly1 ` CCfld ) ) e. Mnd )
184 160 183 mp1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( mulGrp ` ( Poly1 ` CCfld ) ) e. Mnd )
185 simpr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> k e. NN0 )
186 114 57 93 vr1cl 
 |-  ( CCfld e. Ring -> ( var1 ` CCfld ) e. ( Base ` ( Poly1 ` CCfld ) ) )
187 13 186 mp1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( var1 ` CCfld ) e. ( Base ` ( Poly1 ` CCfld ) ) )
188 182 116 184 185 187 mulgnn0cld 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) )
189 57 ply1sca 
 |-  ( CCfld e. Ring -> CCfld = ( Scalar ` ( Poly1 ` CCfld ) ) )
190 13 189 ax-mp 
 |-  CCfld = ( Scalar ` ( Poly1 ` CCfld ) )
191 93 190 153 8 lmodvscl 
 |-  ( ( ( Poly1 ` CCfld ) e. LMod /\ ( ( coe1 ` a ) ` k ) e. CC /\ ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) ) -> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) e. ( Base ` ( Poly1 ` CCfld ) ) )
192 172 181 188 191 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) e. ( Base ` ( Poly1 ` CCfld ) ) )
193 192 fmpttd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) : NN0 --> ( Base ` ( Poly1 ` CCfld ) ) )
194 165 mptex 
 |-  ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) e. _V
195 funmpt 
 |-  Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) )
196 fvex 
 |-  ( 0g ` ( Poly1 ` CCfld ) ) e. _V
197 194 195 196 3pm3.2i 
 |-  ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) /\ ( 0g ` ( Poly1 ` CCfld ) ) e. _V )
198 197 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) /\ ( 0g ` ( Poly1 ` CCfld ) ) e. _V ) )
199 154 93 57 21 coe1sfi 
 |-  ( a e. ( Base ` ( Poly1 ` CCfld ) ) -> ( coe1 ` a ) finSupp 0 )
200 152 199 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( coe1 ` a ) finSupp 0 )
201 200 fsuppimpd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( coe1 ` a ) supp 0 ) e. Fin )
202 179 feqmptd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( coe1 ` a ) = ( k e. NN0 |-> ( ( coe1 ` a ) ` k ) ) )
203 202 oveq1d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( ( coe1 ` a ) ` k ) ) supp 0 ) )
204 eqimss2 
 |-  ( ( ( coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( ( coe1 ` a ) ` k ) ) supp 0 ) -> ( ( k e. NN0 |-> ( ( coe1 ` a ) ` k ) ) supp 0 ) C_ ( ( coe1 ` a ) supp 0 ) )
205 203 204 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( ( coe1 ` a ) ` k ) ) supp 0 ) C_ ( ( coe1 ` a ) supp 0 ) )
206 13 171 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( Poly1 ` CCfld ) e. LMod )
207 93 190 153 21 158 lmod0vs 
 |-  ( ( ( Poly1 ` CCfld ) e. LMod /\ x e. ( Base ` ( Poly1 ` CCfld ) ) ) -> ( 0 ( .s ` ( Poly1 ` CCfld ) ) x ) = ( 0g ` ( Poly1 ` CCfld ) ) )
208 206 207 sylan 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ x e. ( Base ` ( Poly1 ` CCfld ) ) ) -> ( 0 ( .s ` ( Poly1 ` CCfld ) ) x ) = ( 0g ` ( Poly1 ` CCfld ) ) )
209 c0ex 
 |-  0 e. _V
210 209 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> 0 e. _V )
211 205 208 180 188 210 suppssov1 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) supp ( 0g ` ( Poly1 ` CCfld ) ) ) C_ ( ( coe1 ` a ) supp 0 ) )
212 suppssfifsupp 
 |-  ( ( ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) /\ ( 0g ` ( Poly1 ` CCfld ) ) e. _V ) /\ ( ( ( coe1 ` a ) supp 0 ) e. Fin /\ ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) supp ( 0g ` ( Poly1 ` CCfld ) ) ) C_ ( ( coe1 ` a ) supp 0 ) ) ) -> ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) finSupp ( 0g ` ( Poly1 ` CCfld ) ) )
213 198 201 211 212 syl12anc 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) finSupp ( 0g ` ( Poly1 ` CCfld ) ) )
214 93 158 162 164 166 170 193 213 gsummhm 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( CCfld ^s CC ) gsum ( E o. ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) ) = ( E ` ( ( Poly1 ` CCfld ) gsum ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) ) )
215 95 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> E : ( Base ` ( Poly1 ` CCfld ) ) --> ( Base ` ( CCfld ^s CC ) ) )
216 215 192 cofmpt 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( E o. ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) = ( k e. NN0 |-> ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) )
217 13 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> CCfld e. Ring )
218 10 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> CC e. _V )
219 95 ffvelcdmi 
 |-  ( ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) e. ( Base ` ( Poly1 ` CCfld ) ) -> ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) e. ( Base ` ( CCfld ^s CC ) ) )
220 192 219 syl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) e. ( Base ` ( CCfld ^s CC ) ) )
221 7 8 67 217 218 220 pwselbas 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) : CC --> CC )
222 221 feqmptd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) = ( z e. CC |-> ( ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ` z ) ) )
223 56 a1i 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> CCfld e. CRing )
224 simpr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> z e. CC )
225 4 114 8 57 93 223 224 evl1vard 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( var1 ` CCfld ) e. ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( E ` ( var1 ` CCfld ) ) ` z ) = z ) )
226 185 adantr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> k e. NN0 )
227 4 57 8 93 223 224 225 116 127 226 evl1expd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( k ( .g ` ( mulGrp ` CCfld ) ) z ) ) )
228 224 226 131 syl2anc 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( k ( .g ` ( mulGrp ` CCfld ) ) z ) = ( z ^ k ) )
229 228 eqeq2d 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( k ( .g ` ( mulGrp ` CCfld ) ) z ) <-> ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( z ^ k ) ) )
230 229 anbi2d 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( k ( .g ` ( mulGrp ` CCfld ) ) z ) ) <-> ( ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( z ^ k ) ) ) )
231 227 230 mpbid 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( E ` ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ` z ) = ( z ^ k ) ) )
232 181 adantr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( coe1 ` a ) ` k ) e. CC )
233 4 57 8 93 223 224 231 232 153 80 evl1vsd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) e. ( Base ` ( Poly1 ` CCfld ) ) /\ ( ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ` z ) = ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
234 233 simprd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ` z ) = ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) )
235 234 mpteq2dva 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( z e. CC |-> ( ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ` z ) ) = ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
236 222 235 eqtrd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) = ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
237 236 mpteq2dva 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( k e. NN0 |-> ( E ` ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) = ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) )
238 216 237 eqtrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( E o. ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) = ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) )
239 238 oveq2d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( CCfld ^s CC ) gsum ( E o. ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) ) ) = ( ( CCfld ^s CC ) gsum ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) )
240 157 214 239 3eqtr2d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( E ` a ) = ( ( CCfld ^s CC ) gsum ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) )
241 10 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> CC e. _V )
242 13 14 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> CCfld e. CMnd )
243 181 adantlr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( ( coe1 ` a ) ` k ) e. CC )
244 37 adantll 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
245 243 244 mulcld 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
246 245 anasss 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ ( z e. CC /\ k e. NN0 ) ) -> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
247 165 mptex 
 |-  ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V
248 funmpt 
 |-  Fun ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
249 247 248 43 3pm3.2i 
 |-  ( ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) /\ ( 0g ` ( CCfld ^s CC ) ) e. _V )
250 249 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) /\ ( 0g ` ( CCfld ^s CC ) ) e. _V ) )
251 fzfid 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) e. Fin )
252 eldifn 
 |-  ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) -> -. k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) )
253 252 adantl 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> -. k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) )
254 152 ad2antrr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> a e. ( Base ` ( Poly1 ` CCfld ) ) )
255 eldifi 
 |-  ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) -> k e. NN0 )
256 255 adantl 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> k e. NN0 )
257 eqid 
 |-  ( deg1 ` CCfld ) = ( deg1 ` CCfld )
258 257 57 93 21 154 deg1ge 
 |-  ( ( a e. ( Base ` ( Poly1 ` CCfld ) ) /\ k e. NN0 /\ ( ( coe1 ` a ) ` k ) =/= 0 ) -> k <_ ( ( deg1 ` CCfld ) ` a ) )
259 258 3expia 
 |-  ( ( a e. ( Base ` ( Poly1 ` CCfld ) ) /\ k e. NN0 ) -> ( ( ( coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` CCfld ) ` a ) ) )
260 254 256 259 syl2anc 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( ( coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` CCfld ) ` a ) ) )
261 0xr 
 |-  0 e. RR*
262 257 57 93 deg1xrcl 
 |-  ( a e. ( Base ` ( Poly1 ` CCfld ) ) -> ( ( deg1 ` CCfld ) ` a ) e. RR* )
263 152 262 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( deg1 ` CCfld ) ` a ) e. RR* )
264 263 ad2antrr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( deg1 ` CCfld ) ` a ) e. RR* )
265 xrmax2 
 |-  ( ( 0 e. RR* /\ ( ( deg1 ` CCfld ) ` a ) e. RR* ) -> ( ( deg1 ` CCfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) )
266 261 264 265 sylancr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( deg1 ` CCfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) )
267 256 nn0red 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> k e. RR )
268 267 rexrd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> k e. RR* )
269 ifcl 
 |-  ( ( ( ( deg1 ` CCfld ) ` a ) e. RR* /\ 0 e. RR* ) -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. RR* )
270 264 261 269 sylancl 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. RR* )
271 xrletr 
 |-  ( ( k e. RR* /\ ( ( deg1 ` CCfld ) ` a ) e. RR* /\ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. RR* ) -> ( ( k <_ ( ( deg1 ` CCfld ) ` a ) /\ ( ( deg1 ` CCfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) -> k <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) )
272 268 264 270 271 syl3anc 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( k <_ ( ( deg1 ` CCfld ) ` a ) /\ ( ( deg1 ` CCfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) -> k <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) )
273 266 272 mpan2d 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( k <_ ( ( deg1 ` CCfld ) ` a ) -> k <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) )
274 260 273 syld 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( ( coe1 ` a ) ` k ) =/= 0 -> k <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) )
275 274 256 jctild 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( ( coe1 ` a ) ` k ) =/= 0 -> ( k e. NN0 /\ k <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) )
276 257 57 93 deg1cl 
 |-  ( a e. ( Base ` ( Poly1 ` CCfld ) ) -> ( ( deg1 ` CCfld ) ` a ) e. ( NN0 u. { -oo } ) )
277 152 276 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( deg1 ` CCfld ) ` a ) e. ( NN0 u. { -oo } ) )
278 elun 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` CCfld ) ` a ) e. NN0 \/ ( ( deg1 ` CCfld ) ` a ) e. { -oo } ) )
279 277 278 sylib 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( ( deg1 ` CCfld ) ` a ) e. NN0 \/ ( ( deg1 ` CCfld ) ` a ) e. { -oo } ) )
280 nn0ge0 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. NN0 -> 0 <_ ( ( deg1 ` CCfld ) ` a ) )
281 280 iftrued 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) = ( ( deg1 ` CCfld ) ` a ) )
282 id 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. NN0 -> ( ( deg1 ` CCfld ) ` a ) e. NN0 )
283 281 282 eqeltrd 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
284 mnflt0 
 |-  -oo < 0
285 mnfxr 
 |-  -oo e. RR*
286 xrltnle 
 |-  ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
287 285 261 286 mp2an 
 |-  ( -oo < 0 <-> -. 0 <_ -oo )
288 284 287 mpbi 
 |-  -. 0 <_ -oo
289 elsni 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> ( ( deg1 ` CCfld ) ` a ) = -oo )
290 289 breq2d 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> ( 0 <_ ( ( deg1 ` CCfld ) ` a ) <-> 0 <_ -oo ) )
291 288 290 mtbiri 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> -. 0 <_ ( ( deg1 ` CCfld ) ` a ) )
292 291 iffalsed 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) = 0 )
293 0nn0 
 |-  0 e. NN0
294 292 293 eqeltrdi 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
295 283 294 jaoi 
 |-  ( ( ( ( deg1 ` CCfld ) ` a ) e. NN0 \/ ( ( deg1 ` CCfld ) ` a ) e. { -oo } ) -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
296 279 295 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
297 296 ad2antrr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
298 fznn0 
 |-  ( if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 -> ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) <-> ( k e. NN0 /\ k <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) )
299 297 298 syl 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) <-> ( k e. NN0 /\ k <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) )
300 275 299 sylibrd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( ( coe1 ` a ) ` k ) =/= 0 -> k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) )
301 300 necon1bd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( -. k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) -> ( ( coe1 ` a ) ` k ) = 0 ) )
302 253 301 mpd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( coe1 ` a ) ` k ) = 0 )
303 302 oveq1d 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
304 255 244 sylan2 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( z ^ k ) e. CC )
305 304 mul02d 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
306 303 305 eqtrd 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) = 0 )
307 306 an32s 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) /\ z e. CC ) -> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) = 0 )
308 307 mpteq2dva 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> 0 ) )
309 fconstmpt 
 |-  ( CC X. { 0 } ) = ( z e. CC |-> 0 )
310 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
311 13 310 ax-mp 
 |-  CCfld e. Mnd
312 7 21 pws0g 
 |-  ( ( CCfld e. Mnd /\ CC e. _V ) -> ( CC X. { 0 } ) = ( 0g ` ( CCfld ^s CC ) ) )
313 311 10 312 mp2an 
 |-  ( CC X. { 0 } ) = ( 0g ` ( CCfld ^s CC ) )
314 309 313 eqtr3i 
 |-  ( z e. CC |-> 0 ) = ( 0g ` ( CCfld ^s CC ) )
315 308 314 eqtrdi 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) = ( 0g ` ( CCfld ^s CC ) ) )
316 315 166 suppss2 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) supp ( 0g ` ( CCfld ^s CC ) ) ) C_ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) )
317 suppssfifsupp 
 |-  ( ( ( ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) /\ ( 0g ` ( CCfld ^s CC ) ) e. _V ) /\ ( ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) e. Fin /\ ( ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) supp ( 0g ` ( CCfld ^s CC ) ) ) C_ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) finSupp ( 0g ` ( CCfld ^s CC ) ) )
318 250 251 316 317 syl12anc 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) finSupp ( 0g ` ( CCfld ^s CC ) ) )
319 7 8 9 241 166 242 246 318 pwsgsum 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( CCfld ^s CC ) gsum ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> ( CCfld gsum ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) )
320 fz0ssnn0 
 |-  ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) C_ NN0
321 resmpt 
 |-  ( ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) C_ NN0 -> ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) |` ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) = ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
322 320 321 ax-mp 
 |-  ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) |` ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) = ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) )
323 322 oveq2i 
 |-  ( CCfld gsum ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) |` ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) = ( CCfld gsum ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
324 13 14 mp1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> CCfld e. CMnd )
325 165 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> NN0 e. _V )
326 245 fmpttd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) : NN0 --> CC )
327 306 325 suppss2 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) supp 0 ) C_ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) )
328 165 mptex 
 |-  ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V
329 funmpt 
 |-  Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) )
330 328 329 209 3pm3.2i 
 |-  ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) /\ 0 e. _V )
331 330 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) /\ 0 e. _V ) )
332 fzfid 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) e. Fin )
333 suppssfifsupp 
 |-  ( ( ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V /\ Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) /\ 0 e. _V ) /\ ( ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) e. Fin /\ ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) supp 0 ) C_ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) -> ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) finSupp 0 )
334 331 332 327 333 syl12anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) finSupp 0 )
335 8 21 324 325 326 327 334 gsumres 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( CCfld gsum ( ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) |` ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) ) = ( CCfld gsum ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) )
336 elfznn0 
 |-  ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) -> k e. NN0 )
337 336 245 sylan2 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) -> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
338 332 337 gsumfsum 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( CCfld gsum ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) = sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) )
339 323 335 338 3eqtr3a 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( CCfld gsum ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) = sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) )
340 339 mpteq2dva 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( z e. CC |-> ( CCfld gsum ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
341 240 319 340 3eqtrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( E ` a ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
342 16 adantr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> S C_ CC )
343 elplyr 
 |-  ( ( S C_ CC /\ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 /\ ( coe1 ` a ) : NN0 --> S ) -> ( z e. CC |-> sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. ( Poly ` S ) )
344 342 296 179 343 syl3anc 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( z e. CC |-> sum_ k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. ( Poly ` S ) )
345 341 344 eqeltrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( E ` a ) e. ( Poly ` S ) )
346 eleq1 
 |-  ( ( E ` a ) = f -> ( ( E ` a ) e. ( Poly ` S ) <-> f e. ( Poly ` S ) ) )
347 345 346 syl5ibcom 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( E ` a ) = f -> f e. ( Poly ` S ) ) )
348 347 rexlimdva 
 |-  ( S e. ( SubRing ` CCfld ) -> ( E. a e. A ( E ` a ) = f -> f e. ( Poly ` S ) ) )
349 151 348 syl5 
 |-  ( S e. ( SubRing ` CCfld ) -> ( f e. ( E " A ) -> f e. ( Poly ` S ) ) )
350 147 349 impbid 
 |-  ( S e. ( SubRing ` CCfld ) -> ( f e. ( Poly ` S ) <-> f e. ( E " A ) ) )
351 350 eqrdv 
 |-  ( S e. ( SubRing ` CCfld ) -> ( Poly ` S ) = ( E " A ) )