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 ffvelrn 
 |-  ( ( 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 syl5ibr 
 |-  ( 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 ffvelrnda 
 |-  ( ( ( 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 ringmgp 
 |-  ( ( Poly1 ` CCfld ) e. Ring -> ( mulGrp ` ( Poly1 ` CCfld ) ) e. Mnd )
183 160 182 mp1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( mulGrp ` ( Poly1 ` CCfld ) ) e. Mnd )
184 simpr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> k e. NN0 )
185 114 57 93 vr1cl 
 |-  ( CCfld e. Ring -> ( var1 ` CCfld ) e. ( Base ` ( Poly1 ` CCfld ) ) )
186 13 185 mp1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( var1 ` CCfld ) e. ( Base ` ( Poly1 ` CCfld ) ) )
187 110 93 mgpbas 
 |-  ( Base ` ( Poly1 ` CCfld ) ) = ( Base ` ( mulGrp ` ( Poly1 ` CCfld ) ) )
188 187 116 mulgnn0cl 
 |-  ( ( ( mulGrp ` ( Poly1 ` CCfld ) ) e. Mnd /\ k e. NN0 /\ ( var1 ` CCfld ) e. ( Base ` ( Poly1 ` CCfld ) ) ) -> ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) )
189 183 184 186 188 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) e. ( Base ` ( Poly1 ` CCfld ) ) )
190 57 ply1sca 
 |-  ( CCfld e. Ring -> CCfld = ( Scalar ` ( Poly1 ` CCfld ) ) )
191 13 190 ax-mp 
 |-  CCfld = ( Scalar ` ( Poly1 ` CCfld ) )
192 93 191 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 ) ) )
193 172 181 189 192 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 ) ) )
194 193 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 ) ) )
195 165 mptex 
 |-  ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) ) e. _V
196 funmpt 
 |-  Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) ( .s ` ( Poly1 ` CCfld ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` CCfld ) ) ) ( var1 ` CCfld ) ) ) )
197 fvex 
 |-  ( 0g ` ( Poly1 ` CCfld ) ) e. _V
198 195 196 197 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 )
199 198 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 ) )
200 154 93 57 21 coe1sfi 
 |-  ( a e. ( Base ` ( Poly1 ` CCfld ) ) -> ( coe1 ` a ) finSupp 0 )
201 152 200 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( coe1 ` a ) finSupp 0 )
202 201 fsuppimpd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( coe1 ` a ) supp 0 ) e. Fin )
203 179 feqmptd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( coe1 ` a ) = ( k e. NN0 |-> ( ( coe1 ` a ) ` k ) ) )
204 203 oveq1d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( coe1 ` a ) supp 0 ) = ( ( k e. NN0 |-> ( ( coe1 ` a ) ` k ) ) supp 0 ) )
205 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 ) )
206 204 205 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( k e. NN0 |-> ( ( coe1 ` a ) ` k ) ) supp 0 ) C_ ( ( coe1 ` a ) supp 0 ) )
207 13 171 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( Poly1 ` CCfld ) e. LMod )
208 93 191 153 21 158 lmod0vs 
 |-  ( ( ( Poly1 ` CCfld ) e. LMod /\ x e. ( Base ` ( Poly1 ` CCfld ) ) ) -> ( 0 ( .s ` ( Poly1 ` CCfld ) ) x ) = ( 0g ` ( Poly1 ` CCfld ) ) )
209 207 208 sylan 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ x e. ( Base ` ( Poly1 ` CCfld ) ) ) -> ( 0 ( .s ` ( Poly1 ` CCfld ) ) x ) = ( 0g ` ( Poly1 ` CCfld ) ) )
210 c0ex 
 |-  0 e. _V
211 210 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> 0 e. _V )
212 206 209 180 189 211 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 ) )
213 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 ) ) )
214 199 202 212 213 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 ) ) )
215 93 158 162 164 166 170 194 214 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 ) ) ) ) ) ) )
216 95 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> E : ( Base ` ( Poly1 ` CCfld ) ) --> ( Base ` ( CCfld ^s CC ) ) )
217 216 193 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 ) ) ) ) ) )
218 13 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> CCfld e. Ring )
219 10 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) -> CC e. _V )
220 95 ffvelrni 
 |-  ( ( ( ( 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 ) ) )
221 193 220 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 ) ) )
222 7 8 67 218 219 221 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 )
223 222 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 ) ) )
224 56 a1i 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> CCfld e. CRing )
225 simpr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> z e. CC )
226 4 114 8 57 93 224 225 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 ) )
227 184 adantr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> k e. NN0 )
228 4 57 8 93 224 225 226 116 127 227 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 ) ) )
229 225 227 131 syl2anc 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( k ( .g ` ( mulGrp ` CCfld ) ) z ) = ( z ^ k ) )
230 229 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 ) ) )
231 230 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 ) ) ) )
232 228 231 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 ) ) )
233 181 adantr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ k e. NN0 ) /\ z e. CC ) -> ( ( coe1 ` a ) ` k ) e. CC )
234 4 57 8 93 224 225 232 233 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 ) ) ) )
235 234 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 ) ) )
236 235 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 ) ) ) )
237 223 236 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 ) ) ) )
238 237 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 ) ) ) ) )
239 217 238 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 ) ) ) ) )
240 239 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 ) ) ) ) ) )
241 157 215 240 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 ) ) ) ) ) )
242 10 a1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> CC e. _V )
243 13 14 mp1i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> CCfld e. CMnd )
244 181 adantlr 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( ( coe1 ` a ) ` k ) e. CC )
245 37 adantll 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
246 244 245 mulcld 
 |-  ( ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) /\ k e. NN0 ) -> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
247 246 anasss 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ ( z e. CC /\ k e. NN0 ) ) -> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) e. CC )
248 165 mptex 
 |-  ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) ) e. _V
249 funmpt 
 |-  Fun ( k e. NN0 |-> ( z e. CC |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) )
250 248 249 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 )
251 250 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 ) )
252 fzfid 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) e. Fin )
253 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 ) ) )
254 253 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 ) ) )
255 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 ) ) )
256 eldifi 
 |-  ( k e. ( NN0 \ ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) ) -> k e. NN0 )
257 256 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 )
258 eqid 
 |-  ( deg1 ` CCfld ) = ( deg1 ` CCfld )
259 258 57 93 21 154 deg1ge 
 |-  ( ( a e. ( Base ` ( Poly1 ` CCfld ) ) /\ k e. NN0 /\ ( ( coe1 ` a ) ` k ) =/= 0 ) -> k <_ ( ( deg1 ` CCfld ) ` a ) )
260 259 3expia 
 |-  ( ( a e. ( Base ` ( Poly1 ` CCfld ) ) /\ k e. NN0 ) -> ( ( ( coe1 ` a ) ` k ) =/= 0 -> k <_ ( ( deg1 ` CCfld ) ` a ) ) )
261 255 257 260 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 ) ) )
262 0xr 
 |-  0 e. RR*
263 258 57 93 deg1xrcl 
 |-  ( a e. ( Base ` ( Poly1 ` CCfld ) ) -> ( ( deg1 ` CCfld ) ` a ) e. RR* )
264 152 263 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( deg1 ` CCfld ) ` a ) e. RR* )
265 264 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* )
266 xrmax2 
 |-  ( ( 0 e. RR* /\ ( ( deg1 ` CCfld ) ` a ) e. RR* ) -> ( ( deg1 ` CCfld ) ` a ) <_ if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) )
267 262 265 266 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 ) )
268 257 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 )
269 268 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* )
270 ifcl 
 |-  ( ( ( ( deg1 ` CCfld ) ` a ) e. RR* /\ 0 e. RR* ) -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. RR* )
271 265 262 270 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* )
272 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 ) ) )
273 269 265 271 272 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 ) ) )
274 267 273 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 ) ) )
275 261 274 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 ) ) )
276 275 257 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 ) ) ) )
277 258 57 93 deg1cl 
 |-  ( a e. ( Base ` ( Poly1 ` CCfld ) ) -> ( ( deg1 ` CCfld ) ` a ) e. ( NN0 u. { -oo } ) )
278 152 277 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( deg1 ` CCfld ) ` a ) e. ( NN0 u. { -oo } ) )
279 elun 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` CCfld ) ` a ) e. NN0 \/ ( ( deg1 ` CCfld ) ` a ) e. { -oo } ) )
280 278 279 sylib 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( ( deg1 ` CCfld ) ` a ) e. NN0 \/ ( ( deg1 ` CCfld ) ` a ) e. { -oo } ) )
281 nn0ge0 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. NN0 -> 0 <_ ( ( deg1 ` CCfld ) ` a ) )
282 281 iftrued 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) = ( ( deg1 ` CCfld ) ` a ) )
283 id 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. NN0 -> ( ( deg1 ` CCfld ) ` a ) e. NN0 )
284 282 283 eqeltrd 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. NN0 -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
285 mnflt0 
 |-  -oo < 0
286 mnfxr 
 |-  -oo e. RR*
287 xrltnle 
 |-  ( ( -oo e. RR* /\ 0 e. RR* ) -> ( -oo < 0 <-> -. 0 <_ -oo ) )
288 286 262 287 mp2an 
 |-  ( -oo < 0 <-> -. 0 <_ -oo )
289 285 288 mpbi 
 |-  -. 0 <_ -oo
290 elsni 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> ( ( deg1 ` CCfld ) ` a ) = -oo )
291 290 breq2d 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> ( 0 <_ ( ( deg1 ` CCfld ) ` a ) <-> 0 <_ -oo ) )
292 289 291 mtbiri 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> -. 0 <_ ( ( deg1 ` CCfld ) ` a ) )
293 292 iffalsed 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) = 0 )
294 0nn0 
 |-  0 e. NN0
295 293 294 eqeltrdi 
 |-  ( ( ( deg1 ` CCfld ) ` a ) e. { -oo } -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
296 284 295 jaoi 
 |-  ( ( ( ( deg1 ` CCfld ) ` a ) e. NN0 \/ ( ( deg1 ` CCfld ) ` a ) e. { -oo } ) -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
297 280 296 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) e. NN0 )
298 297 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 )
299 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 ) ) ) )
300 298 299 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 ) ) ) )
301 276 300 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 ) ) ) )
302 301 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 ) )
303 254 302 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 )
304 303 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 ) ) )
305 256 245 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 )
306 305 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 )
307 304 306 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 )
308 307 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 )
309 308 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 ) )
310 fconstmpt 
 |-  ( CC X. { 0 } ) = ( z e. CC |-> 0 )
311 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
312 13 311 ax-mp 
 |-  CCfld e. Mnd
313 7 21 pws0g 
 |-  ( ( CCfld e. Mnd /\ CC e. _V ) -> ( CC X. { 0 } ) = ( 0g ` ( CCfld ^s CC ) ) )
314 312 10 313 mp2an 
 |-  ( CC X. { 0 } ) = ( 0g ` ( CCfld ^s CC ) )
315 310 314 eqtr3i 
 |-  ( z e. CC |-> 0 ) = ( 0g ` ( CCfld ^s CC ) )
316 309 315 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 ) ) )
317 316 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 ) ) )
318 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 ) ) )
319 251 252 317 318 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 ) ) )
320 7 8 9 242 166 243 247 319 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 ) ) ) ) ) )
321 fz0ssnn0 
 |-  ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) C_ NN0
322 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 ) ) ) )
323 321 322 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 ) ) )
324 323 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 ) ) ) )
325 13 14 mp1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> CCfld e. CMnd )
326 165 a1i 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> NN0 e. _V )
327 246 fmpttd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) : NN0 --> CC )
328 307 326 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 ) ) )
329 165 mptex 
 |-  ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) e. _V
330 funmpt 
 |-  Fun ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) )
331 329 330 210 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 )
332 331 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 ) )
333 fzfid 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) e. Fin )
334 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 )
335 332 333 328 334 syl12anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) /\ z e. CC ) -> ( k e. NN0 |-> ( ( ( coe1 ` a ) ` k ) x. ( z ^ k ) ) ) finSupp 0 )
336 8 21 325 326 327 328 335 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 ) ) ) ) )
337 elfznn0 
 |-  ( k e. ( 0 ... if ( 0 <_ ( ( deg1 ` CCfld ) ` a ) , ( ( deg1 ` CCfld ) ` a ) , 0 ) ) -> k e. NN0 )
338 337 246 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 )
339 333 338 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 ) ) )
340 324 336 339 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 ) ) )
341 340 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 ) ) ) )
342 241 320 341 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 ) ) ) )
343 16 adantr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> S C_ CC )
344 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 ) )
345 343 297 179 344 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 ) )
346 342 345 eqeltrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( E ` a ) e. ( Poly ` S ) )
347 eleq1 
 |-  ( ( E ` a ) = f -> ( ( E ` a ) e. ( Poly ` S ) <-> f e. ( Poly ` S ) ) )
348 346 347 syl5ibcom 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ a e. A ) -> ( ( E ` a ) = f -> f e. ( Poly ` S ) ) )
349 348 rexlimdva 
 |-  ( S e. ( SubRing ` CCfld ) -> ( E. a e. A ( E ` a ) = f -> f e. ( Poly ` S ) ) )
350 151 349 syl5 
 |-  ( S e. ( SubRing ` CCfld ) -> ( f e. ( E " A ) -> f e. ( Poly ` S ) ) )
351 147 350 impbid 
 |-  ( S e. ( SubRing ` CCfld ) -> ( f e. ( Poly ` S ) <-> f e. ( E " A ) ) )
352 351 eqrdv 
 |-  ( S e. ( SubRing ` CCfld ) -> ( Poly ` S ) = ( E " A ) )