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

Theorem plypf1 23152
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 23135 . . . . 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 465 . . . 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 2422 . . . . . . . . 9  |-  (fld  ^s  CC )  =  (fld 
^s 
CC )
4 cnfldbas 18961 . . . . . . . . 9  |-  CC  =  ( Base ` fld )
5 eqid 2422 . . . . . . . . 9  |-  ( 0g
`  (fld 
^s 
CC ) )  =  ( 0g `  (fld  ^s  CC ) )
6 cnex 9620 . . . . . . . . . 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 12185 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( 0 ... n
)  e.  Fin )
9 cnring 18977 . . . . . . . . . 10  |-fld  e.  Ring
10 ringcmn 17798 . . . . . . . . . 10  |-  (fld  e.  Ring  ->fld  e. CMnd )
119, 10mp1i 13 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->fld  e. CMnd )
124subrgss 17996 . . . . . . . . . . . . 13  |-  ( S  e.  (SubRing ` fld )  ->  S  C_  CC )
1312ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  S  C_  CC )
14 elmapi 7497 . . . . . . . . . . . . . . 15  |-  ( a  e.  ( ( S  u.  { 0 } )  ^m  NN0 )  ->  a : NN0 --> ( S  u.  { 0 } ) )
1514ad2antll 733 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> ( S  u.  { 0 } ) )
16 subrgsubg 18001 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubRing ` fld )  ->  S  e.  (SubGrp ` fld ) )
17 cnfld0 18979 . . . . . . . . . . . . . . . . . . . 20  |-  0  =  ( 0g ` fld )
1817subg0cl 16812 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubGrp ` fld )  ->  0  e.  S )
1916, 18syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( S  e.  (SubRing ` fld )  ->  0  e.  S )
2019adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
0  e.  S )
2120snssd 4142 . . . . . . . . . . . . . . . 16  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  { 0 }  C_  S )
22 ssequn2 3639 . . . . . . . . . . . . . . . 16  |-  ( { 0 }  C_  S  <->  ( S  u.  { 0 } )  =  S )
2321, 22sylib 199 . . . . . . . . . . . . . . 15  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( S  u.  {
0 } )  =  S )
2423feq3d 5730 . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> S )
26 elfznn0 11887 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... n )  ->  k  e.  NN0 )
27 ffvelrn 6031 . . . . . . . . . . . . 13  |-  ( ( a : NN0 --> S  /\  k  e.  NN0 )  -> 
( a `  k
)  e.  S )
2825, 26, 27syl2an 479 . . . . . . . . . . . 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 3465 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( a `  k )  e.  CC )
3029adantrl 720 . . . . . . . . . 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 762 . . . . . . . . . . 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 733 . . . . . . . . . . 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 12289 . . . . . . . . . . 11  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( z ^ k
)  e.  CC )
3431, 32, 33syl2anc 665 . . . . . . . . . 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 9663 . . . . . . . . 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 2422 . . . . . . . . . 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 6147 . . . . . . . . . . 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 5887 . . . . . . . . . . 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 7896 . . . . . . . . 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 17598 . . . . . . . 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 12185 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  z  e.  CC )  ->  ( 0 ... n
)  e.  Fin )
4435anassrs 652 . . . . . . . . . 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 19021 . . . . . . . . 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 4507 . . . . . . . 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 2463 . . . . . . 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 17830 . . . . . . . . . 10  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  (fld 
^s 
CC )  e.  Ring )
499, 6, 48mp2an 676 . . . . . . . . 9  |-  (fld  ^s  CC )  e.  Ring
50 ringcmn 17798 . . . . . . . . 9  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e. CMnd )
5149, 50mp1i 13 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
(fld  ^s  CC )  e. CMnd )
52 cncrng 18976 . . . . . . . . . . 11  |-fld  e.  CRing
53 plypf1.e . . . . . . . . . . . 12  |-  E  =  (eval1 ` fld )
54 eqid 2422 . . . . . . . . . . . 12  |-  (Poly1 ` fld )  =  (Poly1 ` fld )
5553, 54, 3, 4evl1rhm 18907 . . . . . . . . . . 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 18813 . . . . . . . . . . 11  |-  ( S  e.  (SubRing ` fld )  ->  A  e.  (SubRing `  (Poly1 ` fld ) ) )
6160adantr 466 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  A  e.  (SubRing `  (Poly1 ` fld )
) )
62 rhmima 18026 . . . . . . . . . 10  |-  ( ( E  e.  ( (Poly1 ` fld ) RingHom 
(fld  ^s  CC ) )  /\  A  e.  (SubRing `  (Poly1 ` fld ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
6356, 61, 62sylancr 667 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
64 subrgsubg 18001 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubGrp `  (fld 
^s 
CC ) ) )
65 subgsubm 16826 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubGrp `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubMnd `  (fld 
^s 
CC ) ) )
6663, 64, 653syl 18 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubMnd `  (fld  ^s  CC ) ) )
67 eqid 2422 . . . . . . . . . . . 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 5785 . . . . . . . . . . . . . 14  |-  ( ( a `  k )  e.  CC  ->  ( CC  X.  { ( a `
 k ) } ) : CC --> CC )
7129, 70syl 17 . . . . . . . . . . . . 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 15373 . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . 13  |-  ( ( CC  X.  { ( a `  k ) } )  e.  (
Base `  (fld  ^s  CC )
)  <->  ( CC  X.  { ( a `  k ) } ) : CC --> CC )
7471, 73sylibr 215 . . . . . . . . . . . 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 814 . . . . . . . . . . . . . 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 2422 . . . . . . . . . . . . . 14  |-  ( z  e.  CC  |->  ( z ^ k ) )  =  ( z  e.  CC  |->  ( z ^
k ) )
7775, 76fmptd 6057 . . . . . . . . . . . . 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 15373 . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . 13  |-  ( ( z  e.  CC  |->  ( z ^ k ) )  e.  ( Base `  (fld 
^s 
CC ) )  <->  ( z  e.  CC  |->  ( z ^
k ) ) : CC --> CC )
8077, 79sylibr 215 . . . . . . . . . . . 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 18963 . . . . . . . . . . . 12  |-  x.  =  ( .r ` fld )
82 eqid 2422 . . . . . . . . . . . 12  |-  ( .r
`  (fld 
^s 
CC ) )  =  ( .r `  (fld  ^s  CC ) )
833, 67, 68, 69, 74, 80, 81, 82pwsmulrval 15376 . . . . . . . . . . 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 466 . . . . . . . . . . . 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 4893 . . . . . . . . . . . . 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 2423 . . . . . . . . . . . 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 6558 . . . . . . . . . . 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 2463 . . . . . . . . . 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 466 . . . . . . . . . . 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 2422 . . . . . . . . . . . . . 14  |-  (algSc `  (Poly1 ` fld ) )  =  (algSc `  (Poly1 ` fld ) )
9253, 54, 4, 91evl1sca 18909 . . . . . . . . . . . . 13  |-  ( (fld  e. 
CRing  /\  ( a `  k )  e.  CC )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  =  ( CC  X.  { ( a `  k ) } ) )
9352, 29, 92sylancr 667 . . . . . . . . . . . 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 2422 . . . . . . . . . . . . . . . 16  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (Poly1 ` fld ) )
9594, 67rhmf 17941 . . . . . . . . . . . . . . 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 5742 . . . . . . . . . . . . . 14  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  E  Fn  ( Base `  (Poly1 ` fld ) ) )
9896, 97mp1i 13 . . . . . . . . . . . . 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 17996 . . . . . . . . . . . . . . 15  |-  ( A  e.  (SubRing `  (Poly1 ` fld )
)  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
10060, 99syl 17 . . . . . . . . . . . . . 14  |-  ( S  e.  (SubRing ` fld )  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
101100ad2antrr 730 . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . 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 18840 . . . . . . . . . . . . . 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 235 . . . . . . . . . . . . 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 6154 . . . . . . . . . . . . 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 1264 . . . . . . . . . . . 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 2511 . . . . . . . . . . 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 17996 . . . . . . . . . . . . . . . . 17  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  C_  ( Base `  (fld 
^s 
CC ) ) )
10990, 108syl 17 . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . 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 2422 . . . . . . . . . . . . . . . . . . . 20  |-  (mulGrp `  (Poly1 ` fld ) )  =  (mulGrp `  (Poly1 ` fld ) )
112111subrgsubm 18008 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  (SubRing `  (Poly1 ` fld )
)  ->  A  e.  (SubMnd `  (mulGrp `  (Poly1 ` fld )
) ) )
113110, 112syl 17 . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  k  e.  NN0 )
115 eqid 2422 . . . . . . . . . . . . . . . . . . 19  |-  (var1 ` fld )  =  (var1 ` fld )
116115, 102, 57, 58, 59subrgvr1cl 18842 . . . . . . . . . . . . . . . . . 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 2422 . . . . . . . . . . . . . . . . . . 19  |-  (.g `  (mulGrp `  (Poly1 ` fld ) ) )  =  (.g `  (mulGrp `  (Poly1 ` fld )
) )
118117submmulgcl 16779 . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . 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 6154 . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . . 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 15374 . . . . . . . . . . . . . 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 5930 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . 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 18912 . . . . . . . . . . . . . . . . 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 2422 . . . . . . . . . . . . . . . . 17  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
129114adantr 466 . . . . . . . . . . . . . . . . 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 18920 . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . 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 18988 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^ k
) )
133126, 129, 132syl2anc 665 . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . 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 4507 . . . . . . . . . . . . 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 2463 . . . . . . . . . . . 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 2511 . . . . . . . . . . 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 18007 . . . . . . . . . . 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 1264 . . . . . . . . . 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 2511 . . . . . . . . 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 6057 . . . . . . . 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 7896 . . . . . . . 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 17539 . . . . . . 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 2511 . . . . . 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 2494 . . . . . 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 225 . . . . 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 2924 . . . 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 33 . . 3  |-  ( S  e.  (SubRing ` fld )  ->  ( f  e.  (Poly `  S
)  ->  f  e.  ( E " A ) ) )
149 ffun 5744 . . . . . 6  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  Fun  E )
15096, 149ax-mp 5 . . . . 5  |-  Fun  E
151 fvelima 5929 . . . . 5  |-  ( ( Fun  E  /\  f  e.  ( E " A
) )  ->  E. a  e.  A  ( E `  a )  =  f )
152150, 151mpan 674 . . . 4  |-  ( f  e.  ( E " A )  ->  E. a  e.  A  ( E `  a )  =  f )
153100sselda 3464 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  a  e.  ( Base `  (Poly1 ` fld )
) )
154 eqid 2422 . . . . . . . . . . . 12  |-  ( .s
`  (Poly1 ` fld ) )  =  ( .s `  (Poly1 ` fld ) )
155 eqid 2422 . . . . . . . . . . . 12  |-  (coe1 `  a
)  =  (coe1 `  a
)
15654, 115, 94, 154, 111, 117, 155ply1coe 18876 . . . . . . . . . . 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 667 . . . . . . . . . 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 5881 . . . . . . . . 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 2422 . . . . . . . . . 10  |-  ( 0g
`  (Poly1 ` fld ) )  =  ( 0g `  (Poly1 ` fld ) )
16054ply1ring 18828 . . . . . . . . . . . 12  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  Ring )
1619, 160ax-mp 5 . . . . . . . . . . 11  |-  (Poly1 ` fld )  e.  Ring
162 ringcmn 17798 . . . . . . . . . . 11  |-  ( (Poly1 ` fld )  e.  Ring  ->  (Poly1 ` fld )  e. CMnd )
163161, 162mp1i 13 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e. CMnd )
164 ringmnd 17776 . . . . . . . . . . 11  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e.  Mnd )
16549, 164mp1i 13 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (fld  ^s  CC )  e.  Mnd )
166 nn0ex 10875 . . . . . . . . . . 11  |-  NN0  e.  _V
167166a1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  NN0  e.  _V )
168 rhmghm 17940 . . . . . . . . . . . 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 16880 . . . . . . . . . . 11  |-  ( E  e.  ( (Poly1 ` fld )  GrpHom  (fld  ^s  CC ) )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
171169, 170mp1i 13 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
17254ply1lmod 18832 . . . . . . . . . . . . 13  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  LMod )
1739, 172mp1i 13 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (Poly1 ` fld )  e.  LMod )
17412ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  S  C_  CC )
175 eqid 2422 . . . . . . . . . . . . . . . . 17  |-  ( Base `  R )  =  (
Base `  R )
176155, 59, 58, 175coe1f 18791 . . . . . . . . . . . . . . . 16  |-  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> (
Base `  R )
)
17757subrgbas 18004 . . . . . . . . . . . . . . . . 17  |-  ( S  e.  (SubRing ` fld )  ->  S  =  ( Base `  R
) )
178177feq3d 5730 . . . . . . . . . . . . . . . 16  |-  ( S  e.  (SubRing ` fld )  ->  ( (coe1 `  a ) : NN0 --> S  <-> 
(coe1 `  a ) : NN0 --> ( Base `  R
) ) )
179176, 178syl5ibr 224 . . . . . . . . . . . . . . 15  |-  ( S  e.  (SubRing ` fld )  ->  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> S ) )
180179imp 430 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a ) : NN0 --> S )
181180ffvelrnda 6033 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  S )
182174, 181sseldd 3465 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  CC )
183111ringmgp 17773 . . . . . . . . . . . . . 14  |-  ( (Poly1 ` fld )  e.  Ring  ->  (mulGrp `  (Poly1 ` fld ) )  e.  Mnd )
184161, 183mp1i 13 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (mulGrp `  (Poly1 ` fld )
)  e.  Mnd )
185 simpr 462 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  k  e.  NN0 )
186115, 54, 94vr1cl 18797 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  -> 
(var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
1879, 186mp1i 13 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
188111, 94mgpbas 17716 . . . . . . . . . . . . . 14  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (mulGrp `  (Poly1 ` fld )
) )
189188, 117mulgnn0cl 16761 . . . . . . . . . . . . 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 1264 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( k
(.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  (
Base `  (Poly1 ` fld ) ) )
19154ply1sca 18833 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  ->fld  =  (Scalar `  (Poly1 ` fld ) ) )
1929, 191ax-mp 5 . . . . . . . . . . . . 13  |-fld  =  (Scalar `  (Poly1 ` fld )
)
19394, 192, 154, 4lmodvscl 18095 . . . . . . . . . . . 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 1264 . . . . . . . . . . 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 2422 . . . . . . . . . . 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 6057 . . . . . . . . . 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 6147 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  e.  _V
198 funmpt 5633 . . . . . . . . . . . . 13  |-  Fun  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )
199 fvex 5887 . . . . . . . . . . . . 13  |-  ( 0g
`  (Poly1 ` fld ) )  e.  _V
200197, 198, 1993pm3.2i 1183 . . . . . . . . . . . 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 18793 . . . . . . . . . . . . 13  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  (coe1 `  a
) finSupp  0 )
203153, 202syl 17 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a ) finSupp  0 )
204203fsuppimpd 7892 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(coe1 `  a ) supp  0
)  e.  Fin )
205180feqmptd 5930 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a )  =  ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) )
206205oveq1d 6316 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(coe1 `  a ) supp  0
)  =  ( ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) supp  0 ) )
207 eqimss2 3517 . . . . . . . . . . . . 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 17 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( (coe1 `  a ) `  k ) ) supp  0
)  C_  ( (coe1 `  a ) supp  0 ) )
2099, 172mp1i 13 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e.  LMod )
21094, 192, 154, 17, 159lmod0vs 18111 . . . . . . . . . . . . 13  |-  ( ( (Poly1 ` fld )  e.  LMod  /\  x  e.  ( Base `  (Poly1 ` fld )
) )  ->  (
0 ( .s `  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
211209, 210sylan 473 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  x  e.  ( Base `  (Poly1 ` fld ) ) )  -> 
( 0 ( .s
`  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
212 c0ex 9637 . . . . . . . . . . . . 13  |-  0  e.  _V
213212a1i 11 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  0  e.  _V )
214208, 211, 181, 190, 213suppssov1 6954 . . . . . . . . . . 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 7900 . . . . . . . . . . 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 1262 . . . . . . . . . 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 17558 . . . . . . . . 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 2423 . . . . . . . . . . . 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 5930 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  =  ( x  e.  ( Base `  (Poly1 ` fld )
)  |->  ( E `  x ) ) )
221 fveq2 5877 . . . . . . . . . . . 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 6067 . . . . . . . . . . 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 6032 . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . 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 15374 . . . . . . . . . . . . . 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 5930 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  z  e.  CC )
23153, 115, 4, 54, 94, 229, 230evl1vard 18912 . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . 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 18920 . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^
k ) )
235234eqeq2d 2436 . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . 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 18919 . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . 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 4507 . . . . . . . . . . . . 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 2463 . . . . . . . . . . . 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 4507 . . . . . . . . . . 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 2463 . . . . . . . . . 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 6317 . . . . . . . . 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 2469 . . . . . . . 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 13 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->fld  e. CMnd )
249182adantlr 719 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
(coe1 `  a ) `  k )  e.  CC )
25033adantll 718 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
z ^ k )  e.  CC )
251249, 250mulcld 9663 . . . . . . . . . 10  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  x.  (
z ^ k ) )  e.  CC )
252251anasss 651 . . . . . . . . 9  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  ( z  e.  CC  /\  k  e. 
NN0 ) )  -> 
( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) )  e.  CC )
253166mptex 6147 . . . . . . . . . . . 12  |-  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) )  e. 
_V
254 funmpt 5633 . . . . . . . . . . . 12  |-  Fun  (
k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) )
255253, 254, 393pm3.2i 1183 . . . . . . . . . . 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 12185 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin )
258 eldifn 3588 . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . . . . . 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 3587 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  ->  k  e.  NN0 )
262261adantl 467 . . . . . . . . . . . . . . . . . . . . . 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 2422 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( deg1  ` fld )  =  ( deg1  ` fld )
264263, 54, 94, 17, 155deg1ge 23033 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0  /\  ( (coe1 `  a ) `  k
)  =/=  0 )  ->  k  <_  (
( deg1  `
fld ) `  a ) )
2652643expia 1207 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  ( ( deg1  ` fld ) `  a ) ) )
266260, 262, 265syl2anc 665 . . . . . . . . . . . . . . . . . . . . 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 9687 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
268263, 54, 94deg1xrcl 23017 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  RR* )
269153, 268syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  RR* )
270269ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 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 11471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\  (
( deg1  `
fld ) `  a )  e.  RR* )  ->  (
( deg1  `
fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )
272267, 270, 271sylancr 667 . . . . . . . . . . . . . . . . . . . . . 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 10926 . . . . . . . . . . . . . . . . . . . . . . . 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 9690 . . . . . . . . . . . . . . . . . . . . . . 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 3951 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  RR*  /\  0  e.  RR* )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
RR* )
276270, 267, 275sylancl 666 . . . . . . . . . . . . . . . . . . . . . . 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 11455 . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . . . . . . . . . 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 45 . . . . . . . . . . . . . . . . . . . 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 545 . . . . . . . . . . . . . . . . . . 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 23018 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  { -oo } ) )
283153, 282syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  ( NN0  u.  { -oo } ) )
284 elun 3606 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  { -oo } )  <->  ( (
( deg1  `
fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
) )
285283, 284sylib 199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
) )
286 nn0ge0 10895 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  0  <_ 
( ( deg1  ` fld ) `  a ) )
287286iftrued 3917 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  ( ( deg1  ` fld ) `  a ) )
288 id 23 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  ( ( deg1  ` fld ) `
 a )  e. 
NN0 )
289287, 288eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
290 mnflt0 11427 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |- -oo  <  0
291 mnfxr 11414 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |- -oo  e.  RR*
292 xrltnle 9701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( -oo  e.  RR*  /\  0  e.  RR* )  ->  ( -oo  <  0  <->  -.  0  <_ -oo ) )
293291, 267, 292mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -oo  <  0  <->  -.  0  <_ -oo )
294290, 293mpbi 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -.  0  <_ -oo
295 elsni 4021 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  ( ( deg1  ` fld ) `  a )  = -oo )
296295breq2d 4432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  ( 0  <_  (
( deg1  `
fld ) `  a )  <->  0  <_ -oo )
)
297294, 296mtbiri 304 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  -.  0  <_  (
( deg1  `
fld ) `  a ) )
298297iffalsed 3920 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  0 )
299 0nn0 10884 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  NN0
300298, 299syl6eqel 2518 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
301289, 300jaoi 380 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
)  ->  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
302285, 301syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
303302ad2antrr 730 . . . . . . . . . . . . . . . . . . . 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 11886 . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . 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 237 . . . . . . . . . . . . . . . . . 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 2642 . . . . . . . . . . . . . . . . 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 6316 . . . . . . . . . . . . . . 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 476 . . . . . . . . . . . . . . . 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 9831 . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . 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 811 . . . . . . . . . . . . 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 4507 . . . . . . . . . . . 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 4893 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( z  e.  CC  |->  0 )
316 ringmnd 17776 . . . . . . . . . . . . . . 15  |-  (fld  e.  Ring  ->fld  e.  Mnd )
3179, 316ax-mp 5 . . . . . . . . . . . . . 14  |-fld  e.  Mnd
3183, 17pws0g 16559 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Mnd  /\  CC  e.  _V )  ->  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) ) )
319317, 6, 318mp2an 676 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) )
320315, 319eqtr3i 2453 . . . . . . . . . . . 12  |-  ( z  e.  CC  |->  0 )  =  ( 0g `  (fld  ^s  CC ) )
321314, 320syl6eq 2479 . . . . . . . . . . 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 6956 . . . . . . . . . 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 7900 . . . . . . . . . 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 1262 . . . . . . . . 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 17598 . . . . . . . 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 11887 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  ->  k  e.  NN0 )
327326ssriv 3468 . . . . . . . . . . . 12  |-  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
C_  NN0
328 resmpt 5169 . . . . . . . . . . . 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 6312 . . . . . . . . . 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 13 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->fld  e. CMnd )
332166a1i 11 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing