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

Theorem plypf1 19991
Description: Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015.)
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 19974 . . . . 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 451 . . . 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 2380 . . . . . . . . 9  |-  (fld  ^s  CC )  =  (fld 
^s 
CC )
4 cnfldbas 16623 . . . . . . . . 9  |-  CC  =  ( Base ` fld )
5 eqid 2380 . . . . . . . . 9  |-  ( 0g
`  (fld 
^s 
CC ) )  =  ( 0g `  (fld  ^s  CC ) )
6 cnex 8997 . . . . . . . . . 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 11232 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( 0 ... n
)  e.  Fin )
9 cnrng 16639 . . . . . . . . . 10  |-fld  e.  Ring
10 rngcmn 15614 . . . . . . . . . 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 15789 . . . . . . . . . . . . 13  |-  ( S  e.  (SubRing ` fld )  ->  S  C_  CC )
1312ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  S  C_  CC )
14 elmapi 6967 . . . . . . . . . . . . . . 15  |-  ( a  e.  ( ( S  u.  { 0 } )  ^m  NN0 )  ->  a : NN0 --> ( S  u.  { 0 } ) )
1514ad2antll 710 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> ( S  u.  { 0 } ) )
16 subrgsubg 15794 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubRing ` fld )  ->  S  e.  (SubGrp ` fld ) )
17 cnfld0 16641 . . . . . . . . . . . . . . . . . . . 20  |-  0  =  ( 0g ` fld )
1817subg0cl 14872 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubGrp ` fld )  ->  0  e.  S )
1916, 18syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( S  e.  (SubRing ` fld )  ->  0  e.  S )
2019adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
0  e.  S )
2120snssd 3879 . . . . . . . . . . . . . . . 16  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  { 0 }  C_  S )
22 ssequn2 3456 . . . . . . . . . . . . . . . 16  |-  ( { 0 }  C_  S  <->  ( S  u.  { 0 } )  =  S )
2321, 22sylib 189 . . . . . . . . . . . . . . 15  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( S  u.  {
0 } )  =  S )
24 feq3 5511 . . . . . . . . . . . . . . 15  |-  ( ( S  u.  { 0 } )  =  S  ->  ( a : NN0 --> ( S  u.  { 0 } )  <->  a : NN0
--> S ) )
2523, 24syl 16 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( a : NN0 --> ( S  u.  { 0 } )  <->  a : NN0
--> S ) )
2615, 25mpbid 202 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> S )
27 elfznn0 11008 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... n )  ->  k  e.  NN0 )
28 ffvelrn 5800 . . . . . . . . . . . . 13  |-  ( ( a : NN0 --> S  /\  k  e.  NN0 )  -> 
( a `  k
)  e.  S )
2926, 27, 28syl2an 464 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( a `  k )  e.  S
)
3013, 29sseldd 3285 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( a `  k )  e.  CC )
3130adantrl 697 . . . . . . . . . 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 )
32 simprl 733 . . . . . . . . . . 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 )
3327ad2antll 710 . . . . . . . . . . 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 )
34 expcl 11319 . . . . . . . . . . 11  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( z ^ k
)  e.  CC )
3532, 33, 34syl2anc 643 . . . . . . . . . 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 )
3631, 35mulcld 9034 . . . . . . . . 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 )
376mptex 5898 . . . . . . . . . . . 12  |-  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) )  e.  _V
3837a1i 11 . . . . . . . . . . 11  |-  ( ( ( 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 eqid 2380 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... n )  |->  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) ) )  =  ( k  e.  ( 0 ... n )  |->  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) ) )
4038, 39fmptd 5825 . . . . . . . . . 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 ) ) ) ) : ( 0 ... n
) --> _V )
418, 40fisuppfi 14693 . . . . . . . . 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 ) ) ) ) " ( _V 
\  { ( 0g
`  (fld 
^s 
CC ) ) } ) )  e.  Fin )
423, 4, 5, 7, 8, 11, 36, 41pwsgsum 15473 . . . . . . . 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 11232 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  z  e.  CC )  ->  ( 0 ... n
)  e.  Fin )
4436anassrs 630 . . . . . . . . . 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 16682 . . . . . . . . 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 4229 . . . . . . . 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 2412 . . . . . . 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 ) ) ) )
483pwsrng 15641 . . . . . . . . . 10  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  (fld 
^s 
CC )  e.  Ring )
499, 6, 48mp2an 654 . . . . . . . . 9  |-  (fld  ^s  CC )  e.  Ring
50 rngcmn 15614 . . . . . . . . 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 16638 . . . . . . . . . . 11  |-fld  e.  CRing
53 plypf1.e . . . . . . . . . . . 12  |-  E  =  (eval1 ` fld )
54 eqid 2380 . . . . . . . . . . . 12  |-  (Poly1 ` fld )  =  (Poly1 ` fld )
5553, 54, 3, 4evl1rhm 19809 . . . . . . . . . . 11  |-  (fld  e.  CRing  ->  E  e.  ( (Poly1 ` fld ) RingHom  (fld  ^s  CC ) ) )
5652, 55ax-mp 8 . . . . . . . . . 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 16547 . . . . . . . . . . 11  |-  ( S  e.  (SubRing ` fld )  ->  A  e.  (SubRing `  (Poly1 ` fld ) ) )
6160adantr 452 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  A  e.  (SubRing `  (Poly1 ` fld )
) )
62 rhmima 15819 . . . . . . . . . 10  |-  ( ( E  e.  ( (Poly1 ` fld ) RingHom 
(fld  ^s  CC ) )  /\  A  e.  (SubRing `  (Poly1 ` fld ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
6356, 61, 62sylancr 645 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
64 subrgsubg 15794 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubGrp `  (fld 
^s 
CC ) ) )
65 subgsubm 14882 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubGrp `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubMnd `  (fld 
^s 
CC ) ) )
6663, 64, 653syl 19 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubMnd `  (fld  ^s  CC ) ) )
67 eqid 2380 . . . . . . . . . . . 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 5565 . . . . . . . . . . . . . 14  |-  ( ( a `  k )  e.  CC  ->  ( CC  X.  { ( a `
 k ) } ) : CC --> CC )
7130, 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 13630 . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . 13  |-  ( ( CC  X.  { ( a `  k ) } )  e.  (
Base `  (fld  ^s  CC )
)  <->  ( CC  X.  { ( a `  k ) } ) : CC --> CC )
7471, 73sylibr 204 . . . . . . . . . . . 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 ) ) )
7535anass1rs 783 . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . 14  |-  ( z  e.  CC  |->  ( z ^ k ) )  =  ( z  e.  CC  |->  ( z ^
k ) )
7775, 76fmptd 5825 . . . . . . . . . . . . 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 13630 . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . 13  |-  ( ( z  e.  CC  |->  ( z ^ k ) )  e.  ( Base `  (fld 
^s 
CC ) )  <->  ( z  e.  CC  |->  ( z ^
k ) ) : CC --> CC )
8077, 79sylibr 204 . . . . . . . . . . . 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 16625 . . . . . . . . . . . 12  |-  x.  =  ( .r ` fld )
82 eqid 2380 . . . . . . . . . . . 12  |-  ( .r
`  (fld 
^s 
CC ) )  =  ( .r `  (fld  ^s  CC ) )
833, 67, 68, 69, 74, 80, 81, 82pwsmulrval 13633 . . . . . . . . . . 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 ) } )  o F  x.  ( z  e.  CC  |->  ( z ^
k ) ) ) )
8430adantr 452 . . . . . . . . . . . 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 4854 . . . . . . . . . . . . 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 2381 . . . . . . . . . . . 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 6254 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( ( CC 
X.  { ( a `
 k ) } )  o F  x.  ( z  e.  CC  |->  ( z ^ k
) ) )  =  ( z  e.  CC  |->  ( ( a `  k )  x.  (
z ^ k ) ) ) )
8983, 88eqtrd 2412 . . . . . . . . . 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 452 . . . . . . . . . . 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 2380 . . . . . . . . . . . . . 14  |-  (algSc `  (Poly1 ` fld ) )  =  (algSc `  (Poly1 ` fld ) )
9253, 54, 4, 91evl1sca 19810 . . . . . . . . . . . . 13  |-  ( (fld  e. 
CRing  /\  ( a `  k )  e.  CC )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  =  ( CC  X.  { ( a `  k ) } ) )
9352, 30, 92sylancr 645 . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . . . 16  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (Poly1 ` fld ) )
9594, 67rhmf 15747 . . . . . . . . . . . . . . 15  |-  ( E  e.  ( (Poly1 ` fld ) RingHom  (fld 
^s 
CC ) )  ->  E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) ) )
9656, 95ax-mp 8 . . . . . . . . . . . . . 14  |-  E :
( Base `  (Poly1 ` fld ) ) --> ( Base `  (fld 
^s 
CC ) )
97 ffn 5524 . . . . . . . . . . . . . 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 15789 . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . 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, 30subrg1asclcl 16573 . . . . . . . . . . . . . 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
) )
10429, 103mpbird 224 . . . . . . . . . . . . 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 5908 . . . . . . . . . . . . 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 1184 . . . . . . . . . . . 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 2455 . . . . . . . . . . 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 15789 . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . . . . . . . 20  |-  (mulGrp `  (Poly1 ` fld ) )  =  (mulGrp `  (Poly1 ` fld ) )
112111subrgsubm 15801 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
11427adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  k  e.  NN0 )
115 eqid 2380 . . . . . . . . . . . . . . . . . . 19  |-  (var1 ` fld )  =  (var1 ` fld )
116115, 102, 57, 58, 59subrgvr1cl 16575 . . . . . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . . . . . . 19  |-  (.g `  (mulGrp `  (Poly1 ` fld ) ) )  =  (.g `  (mulGrp `  (Poly1 ` fld )
) )
118117submmulgcl 14844 . . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . . 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 5908 . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . 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 3285 . . . . . . . . . . . . . . 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 13631 . . . . . . . . . . . . . 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 5711 . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . 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 19813 . . . . . . . . . . . . . . . . 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 2380 . . . . . . . . . . . . . . . . 17  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
129114adantr 452 . . . . . . . . . . . . . . . . 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 19818 . . . . . . . . . . . . . . . 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 450 . . . . . . . . . . . . . . 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 16650 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^ k
) )
133126, 129, 132syl2anc 643 . . . . . . . . . . . . . . 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 2412 . . . . . . . . . . . . . 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 4229 . . . . . . . . . . . . 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 2412 . . . . . . . . . . . 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 2455 . . . . . . . . . . 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 15800 . . . . . . . . . . 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 1184 . . . . . . . . . 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 2455 . . . . . . . . 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, 39fmptd 5825 . . . . . . . 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 ) )
1428, 141fisuppfi 14693 . . . . . . . 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 ) ) ) ) " ( _V 
\  { ( 0g
`  (fld 
^s 
CC ) ) } ) )  e.  Fin )
1435, 51, 8, 66, 141, 142gsumsubmcl 15444 . . . . . . 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 2455 . . . . . 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 2440 . . . . . 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 214 . . . . 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 2773 . . . 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 30 . . 3  |-  ( S  e.  (SubRing ` fld )  ->  ( f  e.  (Poly `  S
)  ->  f  e.  ( E " A ) ) )
149 ffun 5526 . . . . . 6  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  Fun  E )
15096, 149ax-mp 8 . . . . 5  |-  Fun  E
151 fvelima 5710 . . . . 5  |-  ( ( Fun  E  /\  f  e.  ( E " A
) )  ->  E. a  e.  A  ( E `  a )  =  f )
152150, 151mpan 652 . . . 4  |-  ( f  e.  ( E " A )  ->  E. a  e.  A  ( E `  a )  =  f )
153100sselda 3284 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  a  e.  ( Base `  (Poly1 ` fld )
) )
154 eqid 2380 . . . . . . . . . . . 12  |-  ( .s
`  (Poly1 ` fld ) )  =  ( .s `  (Poly1 ` fld ) )
155 eqid 2380 . . . . . . . . . . . 12  |-  (coe1 `  a
)  =  (coe1 `  a
)
156 cnfldex 16622 . . . . . . . . . . . 12  |-fld  e.  _V
15754, 115, 94, 154, 111, 117, 155, 156ply1coe 16604 . . . . . . . . . . 11  |-  ( (fld  e. 
CRing  /\  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 ) ) ) ) ) )
15852, 153, 157sylancr 645 . . . . . . . . . 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 ) ) ) ) ) )
159158fveq2d 5665 . . . . . . . . 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 ) ) ) ) ) ) )
160 eqid 2380 . . . . . . . . . 10  |-  ( 0g
`  (Poly1 ` fld ) )  =  ( 0g `  (Poly1 ` fld ) )
16154ply1rng 16562 . . . . . . . . . . . 12  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  Ring )
1629, 161ax-mp 8 . . . . . . . . . . 11  |-  (Poly1 ` fld )  e.  Ring
163 rngcmn 15614 . . . . . . . . . . 11  |-  ( (Poly1 ` fld )  e.  Ring  ->  (Poly1 ` fld )  e. CMnd )
164162, 163mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e. CMnd )
165 rngmnd 15593 . . . . . . . . . . 11  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e.  Mnd )
16649, 165mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (fld  ^s  CC )  e.  Mnd )
167 nn0ex 10152 . . . . . . . . . . 11  |-  NN0  e.  _V
168167a1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  NN0  e.  _V )
169 rhmghm 15746 . . . . . . . . . . . 12  |-  ( E  e.  ( (Poly1 ` fld ) RingHom  (fld 
^s 
CC ) )  ->  E  e.  ( (Poly1 ` fld )  GrpHom  (fld 
^s 
CC ) ) )
17056, 169ax-mp 8 . . . . . . . . . . 11  |-  E  e.  ( (Poly1 ` fld )  GrpHom  (fld 
^s 
CC ) )
171 ghmmhm 14936 . . . . . . . . . . 11  |-  ( E  e.  ( (Poly1 ` fld )  GrpHom  (fld  ^s  CC ) )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
172170, 171mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
17354ply1lmod 16566 . . . . . . . . . . . . 13  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  LMod )
1749, 173mp1i 12 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (Poly1 ` fld )  e.  LMod )
17512ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  S  C_  CC )
176 eqid 2380 . . . . . . . . . . . . . . . . 17  |-  ( Base `  R )  =  (
Base `  R )
177155, 59, 58, 176coe1f 16529 . . . . . . . . . . . . . . . 16  |-  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> (
Base `  R )
)
17857subrgbas 15797 . . . . . . . . . . . . . . . . 17  |-  ( S  e.  (SubRing ` fld )  ->  S  =  ( Base `  R
) )
179 feq3 5511 . . . . . . . . . . . . . . . . 17  |-  ( S  =  ( Base `  R
)  ->  ( (coe1 `  a ) : NN0 --> S  <-> 
(coe1 `  a ) : NN0 --> ( Base `  R
) ) )
180178, 179syl 16 . . . . . . . . . . . . . . . 16  |-  ( S  e.  (SubRing ` fld )  ->  ( (coe1 `  a ) : NN0 --> S  <-> 
(coe1 `  a ) : NN0 --> ( Base `  R
) ) )
181177, 180syl5ibr 213 . . . . . . . . . . . . . . 15  |-  ( S  e.  (SubRing ` fld )  ->  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> S ) )
182181imp 419 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a ) : NN0 --> S )
183182ffvelrnda 5802 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  S )
184175, 183sseldd 3285 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  CC )
185111rngmgp 15590 . . . . . . . . . . . . . 14  |-  ( (Poly1 ` fld )  e.  Ring  ->  (mulGrp `  (Poly1 ` fld ) )  e.  Mnd )
186162, 185mp1i 12 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (mulGrp `  (Poly1 ` fld )
)  e.  Mnd )
187 simpr 448 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  k  e.  NN0 )
188115, 54, 94vr1cl 16531 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  -> 
(var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
1899, 188mp1i 12 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
190111, 94mgpbas 15574 . . . . . . . . . . . . . 14  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (mulGrp `  (Poly1 ` fld )
) )
191190, 117mulgnn0cl 14826 . . . . . . . . . . . . 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 ) ) )
192186, 187, 189, 191syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( k
(.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  (
Base `  (Poly1 ` fld ) ) )
19354ply1sca 16567 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  ->fld  =  (Scalar `  (Poly1 ` fld ) ) )
1949, 193ax-mp 8 . . . . . . . . . . . . 13  |-fld  =  (Scalar `  (Poly1 ` fld )
)
19594, 194, 154, 4lmodvscl 15887 . . . . . . . . . . . 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 ) ) )
196174, 184, 192, 195syl3anc 1184 . . . . . . . . . . 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 )
) )
197 eqid 2380 . . . . . . . . . . 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 ) ) ) )
198196, 197fmptd 5825 . . . . . . . . . 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 ) ) )
199155, 94, 54, 17coe1sfi 16530 . . . . . . . . . . . 12  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( `' (coe1 `  a ) " ( _V  \  { 0 } ) )  e.  Fin )
200153, 199syl 16 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' (coe1 `  a ) "
( _V  \  {
0 } ) )  e.  Fin )
201182feqmptd 5711 . . . . . . . . . . . . . . 15  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a )  =  ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) )
202201cnveqd 4981 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  `' (coe1 `  a )  =  `' ( k  e.  NN0  |->  ( (coe1 `  a ) `  k ) ) )
203202imaeq1d 5135 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' (coe1 `  a ) "
( _V  \  {
0 } ) )  =  ( `' ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) " ( _V  \  { 0 } ) ) )
204 eqimss2 3337 . . . . . . . . . . . . 13  |-  ( ( `' (coe1 `  a ) "
( _V  \  {
0 } ) )  =  ( `' ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) " ( _V  \  { 0 } ) )  ->  ( `' ( k  e. 
NN0  |->  ( (coe1 `  a
) `  k )
) " ( _V 
\  { 0 } ) )  C_  ( `' (coe1 `  a ) "
( _V  \  {
0 } ) ) )
205203, 204syl 16 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' ( k  e. 
NN0  |->  ( (coe1 `  a
) `  k )
) " ( _V 
\  { 0 } ) )  C_  ( `' (coe1 `  a ) "
( _V  \  {
0 } ) ) )
2069, 173mp1i 12 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e.  LMod )
20794, 194, 154, 17, 160lmod0vs 15903 . . . . . . . . . . . . 13  |-  ( ( (Poly1 ` fld )  e.  LMod  /\  x  e.  ( Base `  (Poly1 ` fld )
) )  ->  (
0 ( .s `  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
208206, 207sylan 458 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  x  e.  ( Base `  (Poly1 ` fld ) ) )  -> 
( 0 ( .s
`  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
209205, 208, 183, 192suppssov1 6234 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' ( k  e. 
NN0  |->  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )
" ( _V  \  { ( 0g `  (Poly1 ` fld ) ) } ) )  C_  ( `' (coe1 `  a ) " ( _V  \  { 0 } ) ) )
210 ssfi 7258 . . . . . . . . . . 11  |-  ( ( ( `' (coe1 `  a
) " ( _V 
\  { 0 } ) )  e.  Fin  /\  ( `' ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )
" ( _V  \  { ( 0g `  (Poly1 ` fld ) ) } ) )  C_  ( `' (coe1 `  a ) " ( _V  \  { 0 } ) ) )  -> 
( `' ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )
" ( _V  \  { ( 0g `  (Poly1 ` fld ) ) } ) )  e.  Fin )
211200, 209, 210syl2anc 643 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' ( k  e. 
NN0  |->  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )
" ( _V  \  { ( 0g `  (Poly1 ` fld ) ) } ) )  e.  Fin )
21294, 160, 164, 166, 168, 172, 198, 211gsummhm 15454 . . . . . . . . 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 ) ) ) ) ) ) )
213 eqidd 2381 . . . . . . . . . . . 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 ) ) ) ) )
21496a1i 11 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) ) )
215214feqmptd 5711 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  =  ( x  e.  ( Base `  (Poly1 ` fld )
)  |->  ( E `  x ) ) )
216 fveq2 5661 . . . . . . . . . . . 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 ) ) ) ) )
217196, 213, 215, 216fmptco 5833 . . . . . . . . . . 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 ) ) ) ) ) )
2189a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->fld  e.  Ring )
2196a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  CC  e.  _V )
22096ffvelrni 5801 . . . . . . . . . . . . . . . 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 ) ) )
221196, 220syl 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 ) ) )
2223, 4, 67, 218, 219, 221pwselbas 13631 . . . . . . . . . . . . . 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 )
223222feqmptd 5711 . . . . . . . . . . . . 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 ) ) )
22452a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->fld  e.  CRing )
225 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  z  e.  CC )
22653, 115, 4, 54, 94, 224, 225evl1vard 19813 . . . . . . . . . . . . . . . . . 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 ) )
227187adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  k  e.  NN0 )
22853, 54, 4, 94, 224, 225, 226, 117, 128, 227evl1expd 19818 . . . . . . . . . . . . . . . . 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 ) ) )
229225, 227, 132syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^
k ) )
230229eqeq2d 2391 . . . . . . . . . . . . . . . . . 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 ) ) )
231230anbi2d 685 . . . . . . . . . . . . . . . . 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 ) ) ) )
232228, 231mpbid 202 . . . . . . . . . . . . . . . 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 ) ) )
233184adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
(coe1 `  a ) `  k )  e.  CC )
23453, 54, 4, 94, 224, 225, 232, 233, 154, 81evl1vsd 19817 . . . . . . . . . . . . . . 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
) ) ) )
235234simprd 450 . . . . . . . . . . . . . 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
) ) )
236235mpteq2dva 4229 . . . . . . . . . . . . 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 ) ) ) )
237223, 236eqtrd 2412 . . . . . . . . . . . 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
) ) ) )
238237mpteq2dva 4229 . . . . . . . . . . 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 ) ) ) ) )
239217, 238eqtrd 2412 . . . . . . . . . 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 ) ) ) ) )
240239oveq2d 6029 . . . . . . . . 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
) ) ) ) ) )
241159, 212, 2403eqtr2d 2418 . . . . . . . 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
) ) ) ) ) )
2426a1i 11 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  CC  e.  _V )
2439, 10mp1i 12 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->fld  e. CMnd )
244184adantlr 696 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
(coe1 `  a ) `  k )  e.  CC )
24534adantll 695 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
z ^ k )  e.  CC )
246244, 245mulcld 9034 . . . . . . . . . 10  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  x.  (
z ^ k ) )  e.  CC )
247246anasss 629 . . . . . . . . 9  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  ( z  e.  CC  /\  k  e. 
NN0 ) )  -> 
( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) )  e.  CC )
248 fzfid 11232 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin )
249 eldifn 3406 . . . . . . . . . . . . . . . . . 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 ) ) )
250249adantl 453 . . . . . . . . . . . . . . . . 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 ) ) )
251153ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 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 )
) )
252 eldifi 3405 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  ->  k  e.  NN0 )
253252adantl 453 . . . . . . . . . . . . . . . . . . . . . 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 )
254 eqid 2380 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( deg1  ` fld )  =  ( deg1  ` fld )
255254, 54, 94, 17, 155deg1ge 19881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0  /\  ( (coe1 `  a ) `  k
)  =/=  0 )  ->  k  <_  (
( deg1  `
fld ) `  a ) )
2562553expia 1155 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  ( ( deg1  ` fld ) `  a ) ) )
257251, 253, 256syl2anc 643 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
258 0xr 9057 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
259254, 54, 94deg1xrcl 19865 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  RR* )
260153, 259syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  RR* )
261260ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 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* )
262 xrmax2 10689 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\  (
( deg1  `
fld ) `  a )  e.  RR* )  ->  (
( deg1  `
fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )
263258, 261, 262sylancr 645 . . . . . . . . . . . . . . . . . . . . . 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 ) )
264253nn0red 10200 . . . . . . . . . . . . . . . . . . . . . . . 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 )
265264rexrd 9060 . . . . . . . . . . . . . . . . . . . . . . 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* )
266 ifcl 3711 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  RR*  /\  0  e.  RR* )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
RR* )
267261, 258, 266sylancl 644 . . . . . . . . . . . . . . . . . . . . . . 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* )
268 xrletr 10673 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
269265, 261, 267, 268syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
270263, 269mpan2d 656 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
271257, 270syld 42 . . . . . . . . . . . . . . . . . . . 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 ) ) )
272271, 253jctild 528 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
273254, 54, 94deg1cl 19866 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  {  -oo } ) )
274153, 273syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  ( NN0  u.  { 
-oo } ) )
275 elun 3424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  { 
-oo } )  <->  ( (
( deg1  `
fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  {  -oo }
) )
276274, 275sylib 189 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  {  -oo }
) )
277 nn0ge0 10172 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  0  <_ 
( ( deg1  ` fld ) `  a ) )
278 iftrue 3681 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  <_  ( ( deg1  ` fld ) `  a )  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  ( ( deg1  ` fld ) `  a ) )
279277, 278syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  ( ( deg1  ` fld ) `  a ) )
280 id 20 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  ( ( deg1  ` fld ) `
 a )  e. 
NN0 )
281279, 280eqeltrd 2454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
282 0re 9017 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  e.  RR
283 mnflt 10647 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  e.  RR  ->  -oo  <  0 )
284282, 283ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  -oo  <  0
285 mnfxr 10639 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  -oo  e.  RR*
286 xrltnle 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 
-oo  e.  RR*  /\  0  e.  RR* )  ->  (  -oo  <  0  <->  -.  0  <_  -oo ) )
287285, 258, 286mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  (  -oo  <  0  <->  -.  0  <_  -oo )
288284, 287mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -.  0  <_  -oo
289 elsni 3774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  ( ( deg1  ` fld ) `  a )  =  -oo )
290289breq2d 4158 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  ( 0  <_  (
( deg1  `
fld ) `  a )  <->  0  <_  -oo ) )
291288, 290mtbiri 295 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  -.  0  <_  (
( deg1  `
fld ) `  a ) )
292 iffalse 3682 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  0  <_  ( ( deg1  ` fld ) `  a )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  0 )
293291, 292syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  0 )
294 0nn0 10161 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  NN0
295293, 294syl6eqel 2468 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
296281, 295jaoi 369 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  {  -oo }
)  ->  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
297276, 296syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
298297ad2antrr 707 . . . . . . . . . . . . . . . . . . . 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 )
299 fznn0 11037 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
300298, 299syl 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 ) ) ) )
301272, 300sylibrd 226 . . . . . . . . . . . . . . . . . 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 ) ) ) )
302301necon1bd 2611 . . . . . . . . . . . . . . . . 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 ) )
303250, 302mpd 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 )
304303oveq1d 6028 . . . . . . . . . . . . . . 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 ) ) )
305252, 245sylan2 461 . . . . . . . . . . . . . . . 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 )
306305mul02d 9189 . . . . . . . . . . . . . . 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 )
307304, 306eqtrd 2412 . . . . . . . . . . . . . 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 )
308307an32s 780 . . . . . . . . . . . . 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 )
309308mpteq2dva 4229 . . . . . . . . . . . 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 ) )
310 fconstmpt 4854 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( z  e.  CC  |->  0 )
311 rngmnd 15593 . . . . . . . . . . . . . . 15  |-  (fld  e.  Ring  ->fld  e.  Mnd )
3129, 311ax-mp 8 . . . . . . . . . . . . . 14  |-fld  e.  Mnd
3133, 17pws0g 14651 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Mnd  /\  CC  e.  _V )  ->  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) ) )
314312, 6, 313mp2an 654 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) )
315310, 314eqtr3i 2402 . . . . . . . . . . . 12  |-  ( z  e.  CC  |->  0 )  =  ( 0g `  (fld  ^s  CC ) )
316309, 315syl6eq 2428 . . . . . . . . . . 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 ) ) )
317316suppss2 6232 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' ( k  e. 
NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k
)  x.  ( z ^ k ) ) ) ) " ( _V  \  { ( 0g
`  (fld 
^s 
CC ) ) } ) )  C_  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
318 ssfi 7258 . . . . . . . . . 10  |-  ( ( ( 0 ... if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin  /\  ( `' ( k  e. 
NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k
)  x.  ( z ^ k ) ) ) ) " ( _V  \  { ( 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
) ) ) )
" ( _V  \  { ( 0g `  (fld  ^s  CC ) ) } ) )  e.  Fin )
319248, 317, 318syl2anc 643 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' ( k  e. 
NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k
)  x.  ( z ^ k ) ) ) ) " ( _V  \  { ( 0g
`  (fld 
^s 
CC ) ) } ) )  e.  Fin )
3203, 4, 5, 242, 168, 243, 247, 319pwsgsum 15473 . . . . . . . 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
) ) ) ) ) )
321 elfznn0 11008 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  ->  k  e.  NN0 )
322321ssriv 3288 . . . . . . . . . . . 12  |-  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
C_  NN0
323 resmpt 5124 . . . . . . . . . . . 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
) ) ) )
324322, 323ax-mp 8 . . . . . . . . . . 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
) ) )
325324oveq2i 6024 . . . . . . . . . 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
) ) ) )
3269, 10mp1i 12 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->fld  e. CMnd )
327167a1i 11 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->  NN0  e.  _V )
328 eqid 2380 . . . . . . . . . . . 12  |-  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )  =  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )
329246, 328fmptd 5825 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) : NN0 --> CC )
330307suppss2 6232 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->  ( `' ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) "
( _V  \  {
0 } ) ) 
C_  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
331 fzfid 11232 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin )
332 ssfi 7258 . . . . . . . . . . . 12  |-  ( ( ( 0 ... if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin  /\  ( `' ( k  e. 
NN0  |->  ( ( (coe1 `  a ) `  k
)  x.  ( z ^ k ) ) ) " ( _V 
\  { 0 } ) )  C_  (
0 ... if ( 0  <_  ( ( deg1  ` fld )