MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  plypf1 Structured version   Unicode version

Theorem plypf1 22482
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.)
Hypotheses
Ref Expression
plypf1.r  |-  R  =  (flds  S )
plypf1.p  |-  P  =  (Poly1 `  R )
plypf1.a  |-  A  =  ( Base `  P
)
plypf1.e  |-  E  =  (eval1 ` fld )
Assertion
Ref Expression
plypf1  |-  ( S  e.  (SubRing ` fld )  ->  (Poly `  S )  =  ( E " A ) )

Proof of Theorem plypf1
Dummy variables  f 
a  k  n  x  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elply 22465 . . . . 5  |-  ( 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 ) ) ) ) )
21simprbi 464 . . . 4  |-  ( 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 ) ) ) )
3 eqid 2443 . . . . . . . . 9  |-  (fld  ^s  CC )  =  (fld 
^s 
CC )
4 cnfldbas 18298 . . . . . . . . 9  |-  CC  =  ( Base ` fld )
5 eqid 2443 . . . . . . . . 9  |-  ( 0g
`  (fld 
^s 
CC ) )  =  ( 0g `  (fld  ^s  CC ) )
6 cnex 9576 . . . . . . . . . 10  |-  CC  e.  _V
76a1i 11 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  CC  e.  _V )
8 fzfid 12062 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( 0 ... n
)  e.  Fin )
9 cnring 18314 . . . . . . . . . 10  |-fld  e.  Ring
10 ringcmn 17103 . . . . . . . . . 10  |-  (fld  e.  Ring  ->fld  e. CMnd )
119, 10mp1i 12 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->fld  e. CMnd )
124subrgss 17304 . . . . . . . . . . . . 13  |-  ( S  e.  (SubRing ` fld )  ->  S  C_  CC )
1312ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  S  C_  CC )
14 elmapi 7442 . . . . . . . . . . . . . . 15  |-  ( a  e.  ( ( S  u.  { 0 } )  ^m  NN0 )  ->  a : NN0 --> ( S  u.  { 0 } ) )
1514ad2antll 728 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> ( S  u.  { 0 } ) )
16 subrgsubg 17309 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubRing ` fld )  ->  S  e.  (SubGrp ` fld ) )
17 cnfld0 18316 . . . . . . . . . . . . . . . . . . . 20  |-  0  =  ( 0g ` fld )
1817subg0cl 16083 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubGrp ` fld )  ->  0  e.  S )
1916, 18syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( S  e.  (SubRing ` fld )  ->  0  e.  S )
2019adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
0  e.  S )
2120snssd 4160 . . . . . . . . . . . . . . . 16  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  { 0 }  C_  S )
22 ssequn2 3662 . . . . . . . . . . . . . . . 16  |-  ( { 0 }  C_  S  <->  ( S  u.  { 0 } )  =  S )
2321, 22sylib 196 . . . . . . . . . . . . . . 15  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( S  u.  {
0 } )  =  S )
2423feq3d 5709 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( a : NN0 --> ( S  u.  { 0 } )  <->  a : NN0
--> S ) )
2515, 24mpbid 210 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> S )
26 elfznn0 11779 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... n )  ->  k  e.  NN0 )
27 ffvelrn 6014 . . . . . . . . . . . . 13  |-  ( ( a : NN0 --> S  /\  k  e.  NN0 )  -> 
( a `  k
)  e.  S )
2825, 26, 27syl2an 477 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( a `  k )  e.  S
)
2913, 28sseldd 3490 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( a `  k )  e.  CC )
3029adantrl 715 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  ( z  e.  CC  /\  k  e.  ( 0 ... n ) ) )  ->  ( a `  k )  e.  CC )
31 simprl 756 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  ( z  e.  CC  /\  k  e.  ( 0 ... n ) ) )  ->  z  e.  CC )
3226ad2antll 728 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  ( z  e.  CC  /\  k  e.  ( 0 ... n ) ) )  ->  k  e.  NN0 )
33 expcl 12163 . . . . . . . . . . 11  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( z ^ k
)  e.  CC )
3431, 32, 33syl2anc 661 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  ( z  e.  CC  /\  k  e.  ( 0 ... n ) ) )  ->  ( z ^ k )  e.  CC )
3530, 34mulcld 9619 . . . . . . . . 9  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  ( z  e.  CC  /\  k  e.  ( 0 ... n ) ) )  ->  ( (
a `  k )  x.  ( z ^ k
) )  e.  CC )
36 eqid 2443 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... n )  |->  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) ) )  =  ( k  e.  ( 0 ... n )  |->  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) ) )
376mptex 6128 . . . . . . . . . . 11  |-  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) )  e.  _V
3837a1i 11 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( z  e.  CC  |->  ( ( a `
 k )  x.  ( z ^ k
) ) )  e. 
_V )
39 fvex 5866 . . . . . . . . . . 11  |-  ( 0g
`  (fld 
^s 
CC ) )  e. 
_V
4039a1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( 0g `  (fld  ^s  CC ) )  e.  _V )
4136, 8, 38, 40fsuppmptdm 7842 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( k  e.  ( 0 ... n ) 
|->  ( z  e.  CC  |->  ( ( a `  k )  x.  (
z ^ k ) ) ) ) finSupp  ( 0g `  (fld 
^s 
CC ) ) )
423, 4, 5, 7, 8, 11, 35, 41pwsgsum 16883 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( (fld 
^s 
CC )  gsumg  ( k  e.  ( 0 ... n ) 
|->  ( z  e.  CC  |->  ( ( a `  k )  x.  (
z ^ k ) ) ) ) )  =  ( z  e.  CC  |->  (fld 
gsumg  ( k  e.  ( 0 ... n ) 
|->  ( ( a `  k )  x.  (
z ^ k ) ) ) ) ) )
43 fzfid 12062 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  z  e.  CC )  ->  ( 0 ... n
)  e.  Fin )
4435anassrs 648 . . . . . . . . . 10  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  z  e.  CC )  /\  k  e.  (
0 ... n ) )  ->  ( ( a `
 k )  x.  ( z ^ k
) )  e.  CC )
4543, 44gsumfsum 18358 . . . . . . . . 9  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  z  e.  CC )  ->  (fld 
gsumg  ( k  e.  ( 0 ... n ) 
|->  ( ( a `  k )  x.  (
z ^ k ) ) ) )  = 
sum_ k  e.  ( 0 ... n ) ( ( a `  k )  x.  (
z ^ k ) ) )
4645mpteq2dva 4523 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( z  e.  CC  |->  (fld  gsumg  (
k  e.  ( 0 ... n )  |->  ( ( a `  k
)  x.  ( z ^ k ) ) ) ) )  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... n ) ( ( a `  k
)  x.  ( z ^ k ) ) ) )
4742, 46eqtrd 2484 . . . . . . 7  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( (fld 
^s 
CC )  gsumg  ( 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 ) ) ) )
483pwsring 17138 . . . . . . . . . 10  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  (fld 
^s 
CC )  e.  Ring )
499, 6, 48mp2an 672 . . . . . . . . 9  |-  (fld  ^s  CC )  e.  Ring
50 ringcmn 17103 . . . . . . . . 9  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e. CMnd )
5149, 50mp1i 12 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
(fld  ^s  CC )  e. CMnd )
52 cncrng 18313 . . . . . . . . . . 11  |-fld  e.  CRing
53 plypf1.e . . . . . . . . . . . 12  |-  E  =  (eval1 ` fld )
54 eqid 2443 . . . . . . . . . . . 12  |-  (Poly1 ` fld )  =  (Poly1 ` fld )
5553, 54, 3, 4evl1rhm 18242 . . . . . . . . . . 11  |-  (fld  e.  CRing  ->  E  e.  ( (Poly1 ` fld ) RingHom  (fld  ^s  CC ) ) )
5652, 55ax-mp 5 . . . . . . . . . 10  |-  E  e.  ( (Poly1 ` fld ) RingHom  (fld 
^s 
CC ) )
57 plypf1.r . . . . . . . . . . . 12  |-  R  =  (flds  S )
58 plypf1.p . . . . . . . . . . . 12  |-  P  =  (Poly1 `  R )
59 plypf1.a . . . . . . . . . . . 12  |-  A  =  ( Base `  P
)
6054, 57, 58, 59subrgply1 18148 . . . . . . . . . . 11  |-  ( S  e.  (SubRing ` fld )  ->  A  e.  (SubRing `  (Poly1 ` fld ) ) )
6160adantr 465 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  A  e.  (SubRing `  (Poly1 ` fld )
) )
62 rhmima 17334 . . . . . . . . . 10  |-  ( ( E  e.  ( (Poly1 ` fld ) RingHom 
(fld  ^s  CC ) )  /\  A  e.  (SubRing `  (Poly1 ` fld ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
6356, 61, 62sylancr 663 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
64 subrgsubg 17309 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubGrp `  (fld 
^s 
CC ) ) )
65 subgsubm 16097 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubGrp `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubMnd `  (fld 
^s 
CC ) ) )
6663, 64, 653syl 20 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubMnd `  (fld  ^s  CC ) ) )
67 eqid 2443 . . . . . . . . . . . 12  |-  ( Base `  (fld 
^s 
CC ) )  =  ( Base `  (fld  ^s  CC ) )
689a1i 11 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->fld 
e.  Ring )
696a1i 11 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  CC  e.  _V )
70 fconst6g 5764 . . . . . . . . . . . . . 14  |-  ( ( a `  k )  e.  CC  ->  ( CC  X.  { ( a `
 k ) } ) : CC --> CC )
7129, 70syl 16 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( CC  X.  { ( a `  k ) } ) : CC --> CC )
723, 4, 67pwselbasb 14762 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  ( ( CC 
X.  { ( a `
 k ) } )  e.  ( Base `  (fld 
^s 
CC ) )  <->  ( CC  X.  { ( a `  k ) } ) : CC --> CC ) )
739, 6, 72mp2an 672 . . . . . . . . . . . . 13  |-  ( ( CC  X.  { ( a `  k ) } )  e.  (
Base `  (fld  ^s  CC )
)  <->  ( CC  X.  { ( a `  k ) } ) : CC --> CC )
7471, 73sylibr 212 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( CC  X.  { ( a `  k ) } )  e.  ( Base `  (fld  ^s  CC ) ) )
7534anass1rs 807 . . . . . . . . . . . . . 14  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( z ^
k )  e.  CC )
76 eqid 2443 . . . . . . . . . . . . . 14  |-  ( z  e.  CC  |->  ( z ^ k ) )  =  ( z  e.  CC  |->  ( z ^
k ) )
7775, 76fmptd 6040 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( z  e.  CC  |->  ( z ^
k ) ) : CC --> CC )
783, 4, 67pwselbasb 14762 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  ( ( z  e.  CC  |->  ( z ^ k ) )  e.  ( Base `  (fld  ^s  CC ) )  <->  ( z  e.  CC  |->  ( z ^
k ) ) : CC --> CC ) )
799, 6, 78mp2an 672 . . . . . . . . . . . . 13  |-  ( ( z  e.  CC  |->  ( z ^ k ) )  e.  ( Base `  (fld 
^s 
CC ) )  <->  ( z  e.  CC  |->  ( z ^
k ) ) : CC --> CC )
8077, 79sylibr 212 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( z  e.  CC  |->  ( z ^
k ) )  e.  ( Base `  (fld  ^s  CC ) ) )
81 cnfldmul 18300 . . . . . . . . . . . 12  |-  x.  =  ( .r ` fld )
82 eqid 2443 . . . . . . . . . . . 12  |-  ( .r
`  (fld 
^s 
CC ) )  =  ( .r `  (fld  ^s  CC ) )
833, 67, 68, 69, 74, 80, 81, 82pwsmulrval 14765 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( ( CC 
X.  { ( a `
 k ) } ) ( .r `  (fld  ^s  CC ) ) ( z  e.  CC  |->  ( z ^ k ) ) )  =  ( ( CC  X.  { ( a `  k ) } )  oF  x.  ( z  e.  CC  |->  ( z ^
k ) ) ) )
8429adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( a `  k )  e.  CC )
85 fconstmpt 5033 . . . . . . . . . . . . 13  |-  ( CC 
X.  { ( a `
 k ) } )  =  ( z  e.  CC  |->  ( a `
 k ) )
8685a1i 11 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( CC  X.  { ( a `  k ) } )  =  ( z  e.  CC  |->  ( a `  k ) ) )
87 eqidd 2444 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( z  e.  CC  |->  ( z ^
k ) )  =  ( z  e.  CC  |->  ( z ^ k
) ) )
8869, 84, 75, 86, 87offval2 6541 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( 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 ) ) ) )
8983, 88eqtrd 2484 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( ( CC 
X.  { ( a `
 k ) } ) ( .r `  (fld  ^s  CC ) ) ( z  e.  CC  |->  ( z ^ k ) ) )  =  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) ) )
9063adantr 465 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E " A )  e.  (SubRing `  (fld 
^s 
CC ) ) )
91 eqid 2443 . . . . . . . . . . . . . 14  |-  (algSc `  (Poly1 ` fld ) )  =  (algSc `  (Poly1 ` fld ) )
9253, 54, 4, 91evl1sca 18244 . . . . . . . . . . . . 13  |-  ( (fld  e. 
CRing  /\  ( a `  k )  e.  CC )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  =  ( CC  X.  { ( a `  k ) } ) )
9352, 29, 92sylancr 663 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  =  ( CC  X.  { ( a `  k ) } ) )
94 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (Poly1 ` fld ) )
9594, 67rhmf 17249 . . . . . . . . . . . . . . 15  |-  ( E  e.  ( (Poly1 ` fld ) RingHom  (fld 
^s 
CC ) )  ->  E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) ) )
9656, 95ax-mp 5 . . . . . . . . . . . . . 14  |-  E :
( Base `  (Poly1 ` fld ) ) --> ( Base `  (fld 
^s 
CC ) )
97 ffn 5721 . . . . . . . . . . . . . 14  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  E  Fn  ( Base `  (Poly1 ` fld ) ) )
9896, 97mp1i 12 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  E  Fn  ( Base `  (Poly1 ` fld ) ) )
9994subrgss 17304 . . . . . . . . . . . . . . 15  |-  ( A  e.  (SubRing `  (Poly1 ` fld )
)  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
10060, 99syl 16 . . . . . . . . . . . . . 14  |-  ( S  e.  (SubRing ` fld )  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
101100ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
102 simpll 753 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  S  e.  (SubRing ` fld ) )
10354, 91, 57, 58, 102, 59, 4, 29subrg1asclcl 18175 . . . . . . . . . . . . . 14  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
)  e.  A  <->  ( a `  k )  e.  S
) )
10428, 103mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
)  e.  A )
105 fnfvima 6135 . . . . . . . . . . . . 13  |-  ( ( E  Fn  ( Base `  (Poly1 ` fld ) )  /\  A  C_  ( Base `  (Poly1 ` fld )
)  /\  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
)  e.  A )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  e.  ( E " A ) )
10698, 101, 104, 105syl3anc 1229 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  e.  ( E " A ) )
10793, 106eqeltrrd 2532 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( CC  X.  { ( a `  k ) } )  e.  ( E " A ) )
10867subrgss 17304 . . . . . . . . . . . . . . . . 17  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  C_  ( Base `  (fld 
^s 
CC ) ) )
10990, 108syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E " A )  C_  ( Base `  (fld 
^s 
CC ) ) )
11060ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  A  e.  (SubRing `  (Poly1 ` fld ) ) )
111 eqid 2443 . . . . . . . . . . . . . . . . . . . 20  |-  (mulGrp `  (Poly1 ` fld ) )  =  (mulGrp `  (Poly1 ` fld ) )
112111subrgsubm 17316 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  (SubRing `  (Poly1 ` fld )
)  ->  A  e.  (SubMnd `  (mulGrp `  (Poly1 ` fld )
) ) )
113110, 112syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  A  e.  (SubMnd `  (mulGrp `  (Poly1 ` fld ) ) ) )
11426adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  k  e.  NN0 )
115 eqid 2443 . . . . . . . . . . . . . . . . . . 19  |-  (var1 ` fld )  =  (var1 ` fld )
116115, 102, 57, 58, 59subrgvr1cl 18177 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  (var1 ` fld )  e.  A )
117 eqid 2443 . . . . . . . . . . . . . . . . . . 19  |-  (.g `  (mulGrp `  (Poly1 ` fld ) ) )  =  (.g `  (mulGrp `  (Poly1 ` fld )
) )
118117submmulgcl 16050 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  (SubMnd `  (mulGrp `  (Poly1 ` fld ) ) )  /\  k  e.  NN0  /\  (var1 ` fld )  e.  A )  ->  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  A
)
119113, 114, 116, 118syl3anc 1229 . . . . . . . . . . . . . . . . 17  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) )  e.  A )
120 fnfvima 6135 . . . . . . . . . . . . . . . . 17  |-  ( ( E  Fn  ( Base `  (Poly1 ` fld ) )  /\  A  C_  ( Base `  (Poly1 ` fld )
)  /\  ( k
(.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  A
)  ->  ( E `  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) )  e.  ( E " A ) )
12198, 101, 119, 120syl3anc 1229 . . . . . . . . . . . . . . . 16  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E `  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) )  e.  ( E " A ) )
122109, 121sseldd 3490 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E `  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) )  e.  (
Base `  (fld  ^s  CC )
) )
1233, 4, 67, 68, 69, 122pwselbas 14763 . . . . . . . . . . . . . 14  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E `  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) : CC --> CC )
124123feqmptd 5911 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E `  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) )  =  ( z  e.  CC  |->  ( ( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z ) ) )
12552a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->fld 
e.  CRing )
126 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  z  e.  CC )
12753, 115, 4, 54, 94, 125, 126evl1vard 18247 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( (var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) )  /\  (
( E `  (var1 ` fld )
) `  z )  =  z ) )
128 eqid 2443 . . . . . . . . . . . . . . . . 17  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
129114adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  k  e.  NN0 )
13053, 54, 4, 94, 125, 126, 127, 117, 128, 129evl1expd 18255 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  (
Base `  (Poly1 ` fld ) )  /\  (
( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z )  =  ( k (.g `  (mulGrp ` fld ) ) z ) ) )
131130simprd 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( ( E `
 ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) `  z
)  =  ( k (.g `  (mulGrp ` fld ) ) z ) )
132 cnfldexp 18325 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^ k
) )
133126, 129, 132syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^
k ) )
134131, 133eqtrd 2484 . . . . . . . . . . . . . 14  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( ( E `
 ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) `  z
)  =  ( z ^ k ) )
135134mpteq2dva 4523 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( z  e.  CC  |->  ( ( E `
 ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) `  z
) )  =  ( z  e.  CC  |->  ( z ^ k ) ) )
136124, 135eqtrd 2484 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E `  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) )  =  ( z  e.  CC  |->  ( z ^ k ) ) )
137136, 121eqeltrrd 2532 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( z  e.  CC  |->  ( z ^
k ) )  e.  ( E " A
) )
13882subrgmcl 17315 . . . . . . . . . . 11  |-  ( ( ( E " A
)  e.  (SubRing `  (fld  ^s  CC ) )  /\  ( CC 
X.  { ( a `
 k ) } )  e.  ( E
" A )  /\  ( z  e.  CC  |->  ( z ^ k
) )  e.  ( E " A ) )  ->  ( ( CC  X.  { ( a `
 k ) } ) ( .r `  (fld  ^s  CC ) ) ( z  e.  CC  |->  ( z ^ k ) ) )  e.  ( E
" A ) )
13990, 107, 137, 138syl3anc 1229 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( ( CC 
X.  { ( a `
 k ) } ) ( .r `  (fld  ^s  CC ) ) ( z  e.  CC  |->  ( z ^ k ) ) )  e.  ( E
" A ) )
14089, 139eqeltrrd 2532 . . . . . . . . 9  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( 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
) )
141140, 36fmptd 6040 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
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 ) )
14236, 8, 140, 40fsuppmptdm 7842 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( k  e.  ( 0 ... n ) 
|->  ( z  e.  CC  |->  ( ( a `  k )  x.  (
z ^ k ) ) ) ) finSupp  ( 0g `  (fld 
^s 
CC ) ) )
1435, 51, 8, 66, 141, 142gsumsubmcl 16804 . . . . . . 7  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( (fld 
^s 
CC )  gsumg  ( k  e.  ( 0 ... n ) 
|->  ( z  e.  CC  |->  ( ( a `  k )  x.  (
z ^ k ) ) ) ) )  e.  ( E " A ) )
14447, 143eqeltrrd 2532 . . . . . 6  |-  ( ( S  e.  (SubRing ` fld )  /\  (
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 ) )
145 eleq1 2515 . . . . . 6  |-  ( 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 ) ) )
146144, 145syl5ibrcom 222 . . . . 5  |-  ( ( S  e.  (SubRing ` fld )  /\  (
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 ) ) )
147146rexlimdvva 2942 . . . 4  |-  ( S  e.  (SubRing ` fld )  ->  ( 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 ) ) )
1482, 147syl5 32 . . 3  |-  ( S  e.  (SubRing ` fld )  ->  ( f  e.  (Poly `  S
)  ->  f  e.  ( E " A ) ) )
149 ffun 5723 . . . . . 6  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  Fun  E )
15096, 149ax-mp 5 . . . . 5  |-  Fun  E
151 fvelima 5910 . . . . 5  |-  ( ( Fun  E  /\  f  e.  ( E " A
) )  ->  E. a  e.  A  ( E `  a )  =  f )
152150, 151mpan 670 . . . 4  |-  ( f  e.  ( E " A )  ->  E. a  e.  A  ( E `  a )  =  f )
153100sselda 3489 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  a  e.  ( Base `  (Poly1 ` fld )
) )
154 eqid 2443 . . . . . . . . . . . 12  |-  ( .s
`  (Poly1 ` fld ) )  =  ( .s `  (Poly1 ` fld ) )
155 eqid 2443 . . . . . . . . . . . 12  |-  (coe1 `  a
)  =  (coe1 `  a
)
15654, 115, 94, 154, 111, 117, 155ply1coe 18211 . . . . . . . . . . 11  |-  ( (fld  e. 
Ring  /\  a  e.  (
Base `  (Poly1 ` fld ) ) )  -> 
a  =  ( (Poly1 ` fld ) 
gsumg  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) ) )
1579, 153, 156sylancr 663 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  a  =  ( (Poly1 ` fld )  gsumg  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) ) )
158157fveq2d 5860 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( E `  a )  =  ( E `  ( (Poly1 ` fld )  gsumg  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) ) ) )
159 eqid 2443 . . . . . . . . . 10  |-  ( 0g
`  (Poly1 ` fld ) )  =  ( 0g `  (Poly1 ` fld ) )
16054ply1ring 18163 . . . . . . . . . . . 12  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  Ring )
1619, 160ax-mp 5 . . . . . . . . . . 11  |-  (Poly1 ` fld )  e.  Ring
162 ringcmn 17103 . . . . . . . . . . 11  |-  ( (Poly1 ` fld )  e.  Ring  ->  (Poly1 ` fld )  e. CMnd )
163161, 162mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e. CMnd )
164 ringmnd 17081 . . . . . . . . . . 11  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e.  Mnd )
16549, 164mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (fld  ^s  CC )  e.  Mnd )
166 nn0ex 10807 . . . . . . . . . . 11  |-  NN0  e.  _V
167166a1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  NN0  e.  _V )
168 rhmghm 17248 . . . . . . . . . . . 12  |-  ( E  e.  ( (Poly1 ` fld ) RingHom  (fld 
^s 
CC ) )  ->  E  e.  ( (Poly1 ` fld )  GrpHom  (fld 
^s 
CC ) ) )
16956, 168ax-mp 5 . . . . . . . . . . 11  |-  E  e.  ( (Poly1 ` fld )  GrpHom  (fld 
^s 
CC ) )
170 ghmmhm 16151 . . . . . . . . . . 11  |-  ( E  e.  ( (Poly1 ` fld )  GrpHom  (fld  ^s  CC ) )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
171169, 170mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
17254ply1lmod 18167 . . . . . . . . . . . . 13  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  LMod )
1739, 172mp1i 12 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (Poly1 ` fld )  e.  LMod )
17412ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  S  C_  CC )
175 eqid 2443 . . . . . . . . . . . . . . . . 17  |-  ( Base `  R )  =  (
Base `  R )
176155, 59, 58, 175coe1f 18124 . . . . . . . . . . . . . . . 16  |-  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> (
Base `  R )
)
17757subrgbas 17312 . . . . . . . . . . . . . . . . 17  |-  ( S  e.  (SubRing ` fld )  ->  S  =  ( Base `  R
) )
178177feq3d 5709 . . . . . . . . . . . . . . . 16  |-  ( S  e.  (SubRing ` fld )  ->  ( (coe1 `  a ) : NN0 --> S  <-> 
(coe1 `  a ) : NN0 --> ( Base `  R
) ) )
179176, 178syl5ibr 221 . . . . . . . . . . . . . . 15  |-  ( S  e.  (SubRing ` fld )  ->  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> S ) )
180179imp 429 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a ) : NN0 --> S )
181180ffvelrnda 6016 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  S )
182174, 181sseldd 3490 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  CC )
183111ringmgp 17078 . . . . . . . . . . . . . 14  |-  ( (Poly1 ` fld )  e.  Ring  ->  (mulGrp `  (Poly1 ` fld ) )  e.  Mnd )
184161, 183mp1i 12 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (mulGrp `  (Poly1 ` fld )
)  e.  Mnd )
185 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  k  e.  NN0 )
186115, 54, 94vr1cl 18132 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  -> 
(var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
1879, 186mp1i 12 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
188111, 94mgpbas 17021 . . . . . . . . . . . . . 14  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (mulGrp `  (Poly1 ` fld )
) )
189188, 117mulgnn0cl 16032 . . . . . . . . . . . . 13  |-  ( ( (mulGrp `  (Poly1 ` fld ) )  e.  Mnd  /\  k  e.  NN0  /\  (var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )  -> 
( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) )  e.  ( Base `  (Poly1 ` fld ) ) )
190184, 185, 187, 189syl3anc 1229 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( k
(.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  (
Base `  (Poly1 ` fld ) ) )
19154ply1sca 18168 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  ->fld  =  (Scalar `  (Poly1 ` fld ) ) )
1929, 191ax-mp 5 . . . . . . . . . . . . 13  |-fld  =  (Scalar `  (Poly1 ` fld )
)
19394, 192, 154, 4lmodvscl 17403 . . . . . . . . . . . 12  |-  ( ( (Poly1 ` fld )  e.  LMod  /\  (
(coe1 `  a ) `  k )  e.  CC  /\  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) )  e.  ( Base `  (Poly1 ` fld ) ) )  -> 
( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) )  e.  (
Base `  (Poly1 ` fld ) ) )
194173, 182, 190, 193syl3anc 1229 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (
(coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) )  e.  ( Base `  (Poly1 ` fld )
) )
195 eqid 2443 . . . . . . . . . . 11  |-  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  =  ( k  e. 
NN0  |->  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )
196194, 195fmptd 6040 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) : NN0 --> ( Base `  (Poly1 ` fld ) ) )
197166mptex 6128 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  e.  _V
198 funmpt 5614 . . . . . . . . . . . . 13  |-  Fun  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )
199 fvex 5866 . . . . . . . . . . . . 13  |-  ( 0g
`  (Poly1 ` fld ) )  e.  _V
200197, 198, 1993pm3.2i 1175 . . . . . . . . . . . 12  |-  ( ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  e.  _V  /\  Fun  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  /\  ( 0g `  (Poly1 ` fld ) )  e.  _V )
201200a1i 11 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  e. 
_V  /\  Fun  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  /\  ( 0g `  (Poly1 ` fld ) )  e.  _V ) )
202155, 94, 54, 17coe1sfi 18126 . . . . . . . . . . . . 13  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  (coe1 `  a
) finSupp  0 )
203153, 202syl 16 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a ) finSupp  0 )
204203fsuppimpd 7838 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(coe1 `  a ) supp  0
)  e.  Fin )
205180feqmptd 5911 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a )  =  ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) )
206205oveq1d 6296 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(coe1 `  a ) supp  0
)  =  ( ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) supp  0 ) )
207 eqimss2 3542 . . . . . . . . . . . . 13  |-  ( ( (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 ) )
208206, 207syl 16 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( (coe1 `  a ) `  k ) ) supp  0
)  C_  ( (coe1 `  a ) supp  0 ) )
2099, 172mp1i 12 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e.  LMod )
21094, 192, 154, 17, 159lmod0vs 17419 . . . . . . . . . . . . 13  |-  ( ( (Poly1 ` fld )  e.  LMod  /\  x  e.  ( Base `  (Poly1 ` fld )
) )  ->  (
0 ( .s `  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
211209, 210sylan 471 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  x  e.  ( Base `  (Poly1 ` fld ) ) )  -> 
( 0 ( .s
`  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
212 c0ex 9593 . . . . . . . . . . . . 13  |-  0  e.  _V
213212a1i 11 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  0  e.  _V )
214208, 211, 181, 190, 213suppssov1 6934 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) supp  ( 0g `  (Poly1 ` fld ) ) )  C_  ( (coe1 `  a ) supp  0
) )
215 suppssfifsupp 7846 . . . . . . . . . . 11  |-  ( ( ( ( k  e. 
NN0  |->  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  e.  _V  /\  Fun  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  /\  ( 0g `  (Poly1 ` fld ) )  e.  _V )  /\  ( ( (coe1 `  a ) supp  0 )  e.  Fin  /\  (
( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) supp  ( 0g `  (Poly1 ` fld ) ) )  C_  ( (coe1 `  a ) supp  0
) ) )  -> 
( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) finSupp  ( 0g `  (Poly1 ` fld ) ) )
216201, 204, 214, 215syl12anc 1227 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) finSupp 
( 0g `  (Poly1 ` fld )
) )
21794, 159, 163, 165, 167, 171, 196, 216gsummhm 16833 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(fld  ^s  CC )  gsumg  ( E  o.  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) ) )  =  ( E `  ( (Poly1 ` fld ) 
gsumg  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) ) ) )
218 eqidd 2444 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  =  ( k  e. 
NN0  |->  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) )
21996a1i 11 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) ) )
220219feqmptd 5911 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  =  ( x  e.  ( Base `  (Poly1 ` fld )
)  |->  ( E `  x ) ) )
221 fveq2 5856 . . . . . . . . . . . 12  |-  ( x  =  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) )  -> 
( E `  x
)  =  ( E `
 ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) )
222194, 218, 220, 221fmptco 6049 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( E  o.  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) )  =  ( k  e.  NN0  |->  ( E `
 ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) ) )
2239a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->fld  e.  Ring )
2246a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  CC  e.  _V )
22596ffvelrni 6015 . . . . . . . . . . . . . . . 16  |-  ( ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) )  e.  ( Base `  (Poly1 ` fld )
)  ->  ( E `  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  e.  ( Base `  (fld  ^s  CC ) ) )
226194, 225syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( E `  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  e.  ( Base `  (fld  ^s  CC ) ) )
2273, 4, 67, 223, 224, 226pwselbas 14763 . . . . . . . . . . . . . 14  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( E `  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) : CC --> CC )
228227feqmptd 5911 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( E `  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  =  ( z  e.  CC  |->  ( ( E `  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) `  z ) ) )
22952a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->fld  e.  CRing )
230 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  z  e.  CC )
23153, 115, 4, 54, 94, 229, 230evl1vard 18247 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
(var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) )  /\  (
( E `  (var1 ` fld )
) `  z )  =  z ) )
232185adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  k  e.  NN0 )
23353, 54, 4, 94, 229, 230, 231, 117, 128, 232evl1expd 18255 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) )  e.  ( Base `  (Poly1 ` fld ) )  /\  (
( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z )  =  ( k (.g `  (mulGrp ` fld ) ) z ) ) )
234230, 232, 132syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^
k ) )
235234eqeq2d 2457 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( ( E `  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) `  z
)  =  ( k (.g `  (mulGrp ` fld ) ) z )  <-> 
( ( E `  ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) `  z
)  =  ( z ^ k ) ) )
236235anbi2d 703 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) )  e.  ( Base `  (Poly1 ` fld ) )  /\  (
( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z )  =  ( k (.g `  (mulGrp ` fld ) ) z ) )  <->  ( ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  (
Base `  (Poly1 ` fld ) )  /\  (
( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z )  =  ( z ^ k ) ) ) )
237233, 236mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) )  e.  ( Base `  (Poly1 ` fld ) )  /\  (
( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z )  =  ( z ^ k ) ) )
238182adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
(coe1 `  a ) `  k )  e.  CC )
23953, 54, 4, 94, 229, 230, 237, 238, 154, 81evl1vsd 18254 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) )  e.  (
Base `  (Poly1 ` fld ) )  /\  (
( E `  (
( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) `
 z )  =  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) )
240239simprd 463 . . . . . . . . . . . . . 14  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( E `  (
( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) `
 z )  =  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) )
241240mpteq2dva 4523 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( z  e.  CC  |->  ( ( E `
 ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) `
 z ) )  =  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k
)  x.  ( z ^ k ) ) ) )
242228, 241eqtrd 2484 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( E `  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  =  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) )
243242mpteq2dva 4523 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
k  e.  NN0  |->  ( E `
 ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) )  =  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) ) )
244222, 243eqtrd 2484 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( E  o.  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) )  =  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) ) )
245244oveq2d 6297 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(fld  ^s  CC )  gsumg  ( E  o.  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) ) )  =  ( (fld 
^s 
CC )  gsumg  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) ) ) )
246158, 217, 2453eqtr2d 2490 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( E `  a )  =  ( (fld  ^s  CC ) 
gsumg  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) ) ) )
2476a1i 11 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  CC  e.  _V )
2489, 10mp1i 12 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->fld  e. CMnd )
249182adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
(coe1 `  a ) `  k )  e.  CC )
25033adantll 713 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
z ^ k )  e.  CC )
251249, 250mulcld 9619 . . . . . . . . . 10  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  x.  (
z ^ k ) )  e.  CC )
252251anasss 647 . . . . . . . . 9  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  ( z  e.  CC  /\  k  e. 
NN0 ) )  -> 
( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) )  e.  CC )
253166mptex 6128 . . . . . . . . . . . 12  |-  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) )  e. 
_V
254 funmpt 5614 . . . . . . . . . . . 12  |-  Fun  (
k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) )
255253, 254, 393pm3.2i 1175 . . . . . . . . . . 11  |-  ( ( 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 `  (fld  ^s  CC ) )  e.  _V )
256255a1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  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 `  (fld  ^s  CC ) )  e.  _V ) )
257 fzfid 12062 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin )
258 eldifn 3612 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  ->  -.  k  e.  ( 0 ... if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
259258adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  -.  k  e.  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
260153ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  a  e.  ( Base `  (Poly1 ` fld )
) )
261 eldifi 3611 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  ->  k  e.  NN0 )
262261adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  k  e.  NN0 )
263 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( deg1  ` fld )  =  ( deg1  ` fld )
264263, 54, 94, 17, 155deg1ge 22372 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0  /\  ( (coe1 `  a ) `  k
)  =/=  0 )  ->  k  <_  (
( deg1  `
fld ) `  a ) )
2652643expia 1199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  ( ( deg1  ` fld ) `  a ) ) )
266260, 262, 265syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  ( ( deg1  ` fld ) `  a ) ) )
267 0xr 9643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
268263, 54, 94deg1xrcl 22355 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  RR* )
269153, 268syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  RR* )
270269ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( deg1  `
fld ) `  a )  e.  RR* )
271 xrmax2 11386 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\  (
( deg1  `
fld ) `  a )  e.  RR* )  ->  (
( deg1  `
fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )
272267, 270, 271sylancr 663 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( deg1  `
fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )
273262nn0red 10859 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  k  e.  RR )
274273rexrd 9646 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  k  e.  RR* )
275 ifcl 3968 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  RR*  /\  0  e.  RR* )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
RR* )
276270, 267, 275sylancl 662 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
RR* )
277 xrletr 11370 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  RR*  /\  (
( deg1  `
fld ) `  a )  e.  RR*  /\  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
RR* )  ->  (
( k  <_  (
( deg1  `
fld ) `  a )  /\  ( ( deg1  ` fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  ->  k  <_  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
278274, 270, 276, 277syl3anc 1229 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( k  <_  (
( deg1  `
fld ) `  a )  /\  ( ( deg1  ` fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  ->  k  <_  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
279272, 278mpan2d 674 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
k  <_  ( ( deg1  ` fld ) `  a )  ->  k  <_  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
280266, 279syld 44 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
281280, 262jctild 543 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  ( k  e.  NN0  /\  k  <_  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )
282263, 54, 94deg1cl 22356 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  { -oo } ) )
283153, 282syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  ( NN0  u.  { -oo } ) )
284 elun 3630 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  { -oo } )  <->  ( (
( deg1  `
fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
) )
285283, 284sylib 196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
) )
286 nn0ge0 10827 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  0  <_ 
( ( deg1  ` fld ) `  a ) )
287286iftrued 3934 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  ( ( deg1  ` fld ) `  a ) )
288 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  ( ( deg1  ` fld ) `
 a )  e. 
NN0 )
289287, 288eqeltrd 2531 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
290 mnflt0 11343 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |- -oo  <  0
291 mnfxr 11332 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |- -oo  e.  RR*
292 xrltnle 9656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( -oo  e.  RR*  /\  0  e.  RR* )  ->  ( -oo  <  0  <->  -.  0  <_ -oo ) )
293291, 267, 292mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -oo  <  0  <->  -.  0  <_ -oo )
294290, 293mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -.  0  <_ -oo
295 elsni 4039 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  ( ( deg1  ` fld ) `  a )  = -oo )
296295breq2d 4449 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  ( 0  <_  (
( deg1  `
fld ) `  a )  <->  0  <_ -oo )
)
297294, 296mtbiri 303 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  -.  0  <_  (
( deg1  `
fld ) `  a ) )
298297iffalsed 3937 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  0 )
299 0nn0 10816 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  NN0
300298, 299syl6eqel 2539 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
301289, 300jaoi 379 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
)  ->  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
302285, 301syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
303302ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
304 fznn0 11778 . . . . . . . . . . . . . . . . . . . 20  |-  ( if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0  ->  ( k  e.  ( 0 ... if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  <-> 
( k  e.  NN0  /\  k  <_  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )
305303, 304syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
k  e.  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  <-> 
( k  e.  NN0  /\  k  <_  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )
306281, 305sylibrd 234 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  e.  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )
307306necon1bd 2661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  ( -.  k  e.  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  ->  ( (coe1 `  a
) `  k )  =  0 ) )
308259, 307mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
(coe1 `  a ) `  k )  =  0 )
309308oveq1d 6296 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  x.  (
z ^ k ) )  =  ( 0  x.  ( z ^
k ) ) )
310261, 250sylan2 474 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
z ^ k )  e.  CC )
311310mul02d 9781 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
0  x.  ( z ^ k ) )  =  0 )
312309, 311eqtrd 2484 . . . . . . . . . . . . . 14  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  x.  (
z ^ k ) )  =  0 )
313312an32s 804 . . . . . . . . . . . . 13  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  /\  z  e.  CC )  ->  (
( (coe1 `  a ) `  k )  x.  (
z ^ k ) )  =  0 )
314313mpteq2dva 4523 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  ( NN0  \  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )  =  ( z  e.  CC  |->  0 ) )
315 fconstmpt 5033 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( z  e.  CC  |->  0 )
316 ringmnd 17081 . . . . . . . . . . . . . . 15  |-  (fld  e.  Ring  ->fld  e.  Mnd )
3179, 316ax-mp 5 . . . . . . . . . . . . . 14  |-fld  e.  Mnd
3183, 17pws0g 15830 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Mnd  /\  CC  e.  _V )  ->  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) ) )
319317, 6, 318mp2an 672 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) )
320315, 319eqtr3i 2474 . . . . . . . . . . . 12  |-  ( z  e.  CC  |->  0 )  =  ( 0g `  (fld  ^s  CC ) )
321314, 320syl6eq 2500 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  ( NN0  \  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )  =  ( 0g `  (fld  ^s  CC ) ) )
322321, 167suppss2 6936 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) ) supp  ( 0g `  (fld  ^s  CC ) ) )  C_  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
323 suppssfifsupp 7846 . . . . . . . . . 10  |-  ( ( ( ( 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 `  (fld 
^s 
CC ) )  e. 
_V )  /\  (
( 0 ... if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin  /\  (
( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) ) supp  ( 0g `  (fld  ^s  CC ) ) )  C_  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) ) finSupp  ( 0g `  (fld 
^s 
CC ) ) )
324256, 257, 322, 323syl12anc 1227 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) ) finSupp  ( 0g `  (fld 
^s 
CC ) ) )
3253, 4, 5, 247, 167, 248, 252, 324pwsgsum 16883 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(fld  ^s  CC )  gsumg  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) ) )  =  ( z  e.  CC  |->  (fld  gsumg  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) ) ) )
326 elfznn0 11779 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  ->  k  e.  NN0 )
327326ssriv 3493 . . . . . . . . . . . 12  |-  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
C_  NN0
328 resmpt 5313 . . . . . . . . . . . 12  |-  ( ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
C_  NN0  ->  ( ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )  |`  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  =  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
|->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) )
329327, 328ax-mp 5 . . . . . . . . . . 11  |-  ( ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )  |`  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  =  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
|->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) )
330329oveq2i 6292 . . . . . . . . . 10  |-  (fld  gsumg  ( ( k  e. 
NN0  |->  ( ( (coe1 `  a ) `  k
)  x.  ( z ^ k ) ) )  |`  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  =  (fld  gsumg  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
|->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) )
3319, 10mp1i 12 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->fld  e. CMnd )
332166a1i 11 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing