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

Theorem plypf1 19594
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 19577 . . . . 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 450 . . . 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 2283 . . . . . . . . 9  |-  (fld  ^s  CC )  =  (fld 
^s 
CC )
4 cnfldbas 16383 . . . . . . . . 9  |-  CC  =  ( Base ` fld )
5 eqid 2283 . . . . . . . . 9  |-  ( 0g
`  (fld 
^s 
CC ) )  =  ( 0g `  (fld  ^s  CC ) )
6 cnex 8818 . . . . . . . . . 10  |-  CC  e.  _V
76a1i 10 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  CC  e.  _V )
8 fzfid 11035 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( 0 ... n
)  e.  Fin )
9 cnrng 16396 . . . . . . . . . 10  |-fld  e.  Ring
10 rngcmn 15371 . . . . . . . . . 10  |-  (fld  e.  Ring  ->fld  e. CMnd )
119, 10mp1i 11 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->fld  e. CMnd )
124subrgss 15546 . . . . . . . . . . . . 13  |-  ( S  e.  (SubRing ` fld )  ->  S  C_  CC )
1312ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  S  C_  CC )
14 elmapi 6792 . . . . . . . . . . . . . . 15  |-  ( a  e.  ( ( S  u.  { 0 } )  ^m  NN0 )  ->  a : NN0 --> ( S  u.  { 0 } ) )
1514ad2antll 709 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> ( S  u.  { 0 } ) )
16 subrgsubg 15551 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubRing ` fld )  ->  S  e.  (SubGrp ` fld ) )
17 cnfld0 16398 . . . . . . . . . . . . . . . . . . . 20  |-  0  =  ( 0g ` fld )
1817subg0cl 14629 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubGrp ` fld )  ->  0  e.  S )
1916, 18syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( S  e.  (SubRing ` fld )  ->  0  e.  S )
2019adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
0  e.  S )
2120snssd 3760 . . . . . . . . . . . . . . . 16  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  { 0 }  C_  S )
22 ssequn2 3348 . . . . . . . . . . . . . . . 16  |-  ( { 0 }  C_  S  <->  ( S  u.  { 0 } )  =  S )
2321, 22sylib 188 . . . . . . . . . . . . . . 15  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( S  u.  {
0 } )  =  S )
24 feq3 5377 . . . . . . . . . . . . . . 15  |-  ( ( S  u.  { 0 } )  =  S  ->  ( a : NN0 --> ( S  u.  { 0 } )  <->  a : NN0
--> S ) )
2523, 24syl 15 . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> S )
27 elfznn0 10822 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... n )  ->  k  e.  NN0 )
28 ffvelrn 5663 . . . . . . . . . . . . 13  |-  ( ( a : NN0 --> S  /\  k  e.  NN0 )  -> 
( a `  k
)  e.  S )
2926, 27, 28syl2an 463 . . . . . . . . . . . 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 3181 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( a `  k )  e.  CC )
3130adantrl 696 . . . . . . . . . 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 732 . . . . . . . . . . 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 709 . . . . . . . . . . 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 11121 . . . . . . . . . . 11  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( z ^ k
)  e.  CC )
3532, 33, 34syl2anc 642 . . . . . . . . . 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 8855 . . . . . . . . 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 5746 . . . . . . . . . . . 12  |-  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) )  e.  _V
3837a1i 10 . . . . . . . . . . 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 2283 . . . . . . . . . . 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 5684 . . . . . . . . . 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 14450 . . . . . . . . 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 15230 . . . . . . . 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 11035 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  z  e.  CC )  ->  ( 0 ... n
)  e.  Fin )
4436anassrs 629 . . . . . . . . . 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 16439 . . . . . . . . 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 4106 . . . . . . . 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 2315 . . . . . . 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 15398 . . . . . . . . . 10  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  (fld 
^s 
CC )  e.  Ring )
499, 6, 48mp2an 653 . . . . . . . . 9  |-  (fld  ^s  CC )  e.  Ring
50 rngcmn 15371 . . . . . . . . 9  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e. CMnd )
5149, 50mp1i 11 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
(fld  ^s  CC )  e. CMnd )
52 cncrng 16395 . . . . . . . . . . 11  |-fld  e.  CRing
53 plypf1.e . . . . . . . . . . . 12  |-  E  =  (eval1 ` fld )
54 eqid 2283 . . . . . . . . . . . 12  |-  (Poly1 ` fld )  =  (Poly1 ` fld )
5553, 54, 3, 4evl1rhm 19412 . . . . . . . . . . 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 16311 . . . . . . . . . . 11  |-  ( S  e.  (SubRing ` fld )  ->  A  e.  (SubRing `  (Poly1 ` fld ) ) )
6160adantr 451 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  A  e.  (SubRing `  (Poly1 ` fld )
) )
62 rhmima 15576 . . . . . . . . . 10  |-  ( ( E  e.  ( (Poly1 ` fld ) RingHom 
(fld  ^s  CC ) )  /\  A  e.  (SubRing `  (Poly1 ` fld ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
6356, 61, 62sylancr 644 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
64 subrgsubg 15551 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubGrp `  (fld 
^s 
CC ) ) )
65 subgsubm 14639 . . . . . . . . 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 2283 . . . . . . . . . . . 12  |-  ( Base `  (fld 
^s 
CC ) )  =  ( Base `  (fld  ^s  CC ) )
689a1i 10 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->fld 
e.  Ring )
696a1i 10 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  CC  e.  _V )
70 fconst6g 5430 . . . . . . . . . . . . . 14  |-  ( ( a `  k )  e.  CC  ->  ( CC  X.  { ( a `
 k ) } ) : CC --> CC )
7130, 70syl 15 . . . . . . . . . . . . 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 13387 . . . . . . . . . . . . . 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 653 . . . . . . . . . . . . 13  |-  ( ( CC  X.  { ( a `  k ) } )  e.  (
Base `  (fld  ^s  CC )
)  <->  ( CC  X.  { ( a `  k ) } ) : CC --> CC )
7471, 73sylibr 203 . . . . . . . . . . . 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 782 . . . . . . . . . . . . . 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 2283 . . . . . . . . . . . . . 14  |-  ( z  e.  CC  |->  ( z ^ k ) )  =  ( z  e.  CC  |->  ( z ^
k ) )
7775, 76fmptd 5684 . . . . . . . . . . . . 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 13387 . . . . . . . . . . . . . 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 653 . . . . . . . . . . . . 13  |-  ( ( z  e.  CC  |->  ( z ^ k ) )  e.  ( Base `  (fld 
^s 
CC ) )  <->  ( z  e.  CC  |->  ( z ^
k ) ) : CC --> CC )
8077, 79sylibr 203 . . . . . . . . . . . 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 16385 . . . . . . . . . . . 12  |-  x.  =  ( .r ` fld )
82 eqid 2283 . . . . . . . . . . . 12  |-  ( .r
`  (fld 
^s 
CC ) )  =  ( .r `  (fld  ^s  CC ) )
833, 67, 68, 69, 74, 80, 81, 82pwsmulrval 13390 . . . . . . . . . . 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 451 . . . . . . . . . . . 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 4732 . . . . . . . . . . . . 13  |-  ( CC 
X.  { ( a `
 k ) } )  =  ( z  e.  CC  |->  ( a `
 k ) )
8685a1i 10 . . . . . . . . . . . 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 2284 . . . . . . . . . . . 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 6095 . . . . . . . . . . 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 2315 . . . . . . . . . 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 451 . . . . . . . . . . 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 2283 . . . . . . . . . . . . . 14  |-  (algSc `  (Poly1 ` fld ) )  =  (algSc `  (Poly1 ` fld ) )
9253, 54, 4, 91evl1sca 19413 . . . . . . . . . . . . 13  |-  ( (fld  e. 
CRing  /\  ( a `  k )  e.  CC )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  =  ( CC  X.  { ( a `  k ) } ) )
9352, 30, 92sylancr 644 . . . . . . . . . . . 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 2283 . . . . . . . . . . . . . . . 16  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (Poly1 ` fld ) )
9594, 67rhmf 15504 . . . . . . . . . . . . . . 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 5389 . . . . . . . . . . . . . 14  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  E  Fn  ( Base `  (Poly1 ` fld ) ) )
9896, 97mp1i 11 . . . . . . . . . . . . 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 15546 . . . . . . . . . . . . . . 15  |-  ( A  e.  (SubRing `  (Poly1 ` fld )
)  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
10060, 99syl 15 . . . . . . . . . . . . . 14  |-  ( S  e.  (SubRing ` fld )  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
101100ad2antrr 706 . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . 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 16337 . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . 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 5756 . . . . . . . . . . . . 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 1182 . . . . . . . . . . . 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 2358 . . . . . . . . . . 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 15546 . . . . . . . . . . . . . . . . 17  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  C_  ( Base `  (fld 
^s 
CC ) ) )
10990, 108syl 15 . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . 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 2283 . . . . . . . . . . . . . . . . . . . 20  |-  (mulGrp `  (Poly1 ` fld ) )  =  (mulGrp `  (Poly1 ` fld ) )
112111subrgsubm 15558 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  (SubRing `  (Poly1 ` fld )
)  ->  A  e.  (SubMnd `  (mulGrp `  (Poly1 ` fld )
) ) )
113110, 112syl 15 . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  k  e.  NN0 )
115 eqid 2283 . . . . . . . . . . . . . . . . . . 19  |-  (var1 ` fld )  =  (var1 ` fld )
116115, 102, 57, 58, 59subrgvr1cl 16339 . . . . . . . . . . . . . . . . . 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 2283 . . . . . . . . . . . . . . . . . . 19  |-  (.g `  (mulGrp `  (Poly1 ` fld ) ) )  =  (.g `  (mulGrp `  (Poly1 ` fld )
) )
118117submmulgcl 14601 . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . 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 5756 . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . 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 3181 . . . . . . . . . . . . . . 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 13388 . . . . . . . . . . . . . 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 5575 . . . . . . . . . . . . 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 10 . . . . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . . . . 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 19416 . . . . . . . . . . . . . . . . 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 2283 . . . . . . . . . . . . . . . . 17  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
129114adantr 451 . . . . . . . . . . . . . . . . 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 19421 . . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . . . 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 16407 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^ k
) )
133126, 129, 132syl2anc 642 . . . . . . . . . . . . . . 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 2315 . . . . . . . . . . . . . 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 4106 . . . . . . . . . . . . 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 2315 . . . . . . . . . . . 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 2358 . . . . . . . . . . 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 15557 . . . . . . . . . . 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 1182 . . . . . . . . . 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 2358 . . . . . . . . 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 5684 . . . . . . . 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 14450 . . . . . . . 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 15201 . . . . . . 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 2358 . . . . . 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 2343 . . . . . 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 213 . . . . 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 2674 . . . 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 28 . . 3  |-  ( S  e.  (SubRing ` fld )  ->  ( f  e.  (Poly `  S
)  ->  f  e.  ( E " A ) ) )
149 ffun 5391 . . . . . 6  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  Fun  E )
15096, 149ax-mp 8 . . . . 5  |-  Fun  E
151 fvelima 5574 . . . . 5  |-  ( ( Fun  E  /\  f  e.  ( E " A
) )  ->  E. a  e.  A  ( E `  a )  =  f )
152150, 151mpan 651 . . . 4  |-  ( f  e.  ( E " A )  ->  E. a  e.  A  ( E `  a )  =  f )
153100sselda 3180 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  a  e.  ( Base `  (Poly1 ` fld )
) )
154 eqid 2283 . . . . . . . . . . . 12  |-  ( .s
`  (Poly1 ` fld ) )  =  ( .s `  (Poly1 ` fld ) )
155 eqid 2283 . . . . . . . . . . . 12  |-  (coe1 `  a
)  =  (coe1 `  a
)
156 cnfldex 16380 . . . . . . . . . . . 12  |-fld  e.  _V
15754, 115, 94, 154, 111, 117, 155, 156ply1coe 16368 . . . . . . . . . . 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 644 . . . . . . . . . 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 5529 . . . . . . . . 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 2283 . . . . . . . . . 10  |-  ( 0g
`  (Poly1 ` fld ) )  =  ( 0g `  (Poly1 ` fld ) )
16154ply1rng 16326 . . . . . . . . . . . 12  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  Ring )
1629, 161ax-mp 8 . . . . . . . . . . 11  |-  (Poly1 ` fld )  e.  Ring
163 rngcmn 15371 . . . . . . . . . . 11  |-  ( (Poly1 ` fld )  e.  Ring  ->  (Poly1 ` fld )  e. CMnd )
164162, 163mp1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e. CMnd )
165 rngmnd 15350 . . . . . . . . . . 11  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e.  Mnd )
16649, 165mp1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (fld  ^s  CC )  e.  Mnd )
167 nn0ex 9971 . . . . . . . . . . 11  |-  NN0  e.  _V
168167a1i 10 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  NN0  e.  _V )
169 rhmghm 15503 . . . . . . . . . . . 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 14693 . . . . . . . . . . 11  |-  ( E  e.  ( (Poly1 ` fld )  GrpHom  (fld  ^s  CC ) )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
172170, 171mp1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
17354ply1lmod 16330 . . . . . . . . . . . . 13  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  LMod )
1749, 173mp1i 11 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (Poly1 ` fld )  e.  LMod )
17512ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  S  C_  CC )
176 eqid 2283 . . . . . . . . . . . . . . . . 17  |-  ( Base `  R )  =  (
Base `  R )
177155, 59, 58, 176coe1f 16292 . . . . . . . . . . . . . . . 16  |-  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> (
Base `  R )
)
17857subrgbas 15554 . . . . . . . . . . . . . . . . 17  |-  ( S  e.  (SubRing ` fld )  ->  S  =  ( Base `  R
) )
179 feq3 5377 . . . . . . . . . . . . . . . . 17  |-  ( S  =  ( Base `  R
)  ->  ( (coe1 `  a ) : NN0 --> S  <-> 
(coe1 `  a ) : NN0 --> ( Base `  R
) ) )
180178, 179syl 15 . . . . . . . . . . . . . . . 16  |-  ( S  e.  (SubRing ` fld )  ->  ( (coe1 `  a ) : NN0 --> S  <-> 
(coe1 `  a ) : NN0 --> ( Base `  R
) ) )
181177, 180syl5ibr 212 . . . . . . . . . . . . . . 15  |-  ( S  e.  (SubRing ` fld )  ->  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> S ) )
182181imp 418 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a ) : NN0 --> S )
183 ffvelrn 5663 . . . . . . . . . . . . . 14  |-  ( ( (coe1 `  a ) : NN0 --> S  /\  k  e.  NN0 )  ->  (
(coe1 `  a ) `  k )  e.  S
)
184182, 183sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  S )
185175, 184sseldd 3181 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  CC )
186111rngmgp 15347 . . . . . . . . . . . . . 14  |-  ( (Poly1 ` fld )  e.  Ring  ->  (mulGrp `  (Poly1 ` fld ) )  e.  Mnd )
187162, 186mp1i 11 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (mulGrp `  (Poly1 ` fld )
)  e.  Mnd )
188 simpr 447 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  k  e.  NN0 )
189115, 54, 94vr1cl 16294 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  -> 
(var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
1909, 189mp1i 11 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
191111, 94mgpbas 15331 . . . . . . . . . . . . . 14  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (mulGrp `  (Poly1 ` fld )
) )
192191, 117mulgnn0cl 14583 . . . . . . . . . . . . 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 ) ) )
193187, 188, 190, 192syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( k
(.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  (
Base `  (Poly1 ` fld ) ) )
19454ply1sca 16331 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  ->fld  =  (Scalar `  (Poly1 ` fld ) ) )
1959, 194ax-mp 8 . . . . . . . . . . . . 13  |-fld  =  (Scalar `  (Poly1 ` fld )
)
19694, 195, 154, 4lmodvscl 15644 . . . . . . . . . . . 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 ) ) )
197174, 185, 193, 196syl3anc 1182 . . . . . . . . . . 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 )
) )
198 eqid 2283 . . . . . . . . . . 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 ) ) ) )
199197, 198fmptd 5684 . . . . . . . . . 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 ) ) )
200155, 94, 54, 17coe1sfi 16293 . . . . . . . . . . . 12  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( `' (coe1 `  a ) " ( _V  \  { 0 } ) )  e.  Fin )
201153, 200syl 15 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' (coe1 `  a ) "
( _V  \  {
0 } ) )  e.  Fin )
202182feqmptd 5575 . . . . . . . . . . . . . . 15  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a )  =  ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) )
203202cnveqd 4857 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  `' (coe1 `  a )  =  `' ( k  e.  NN0  |->  ( (coe1 `  a ) `  k ) ) )
204203imaeq1d 5011 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' (coe1 `  a ) "
( _V  \  {
0 } ) )  =  ( `' ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) " ( _V  \  { 0 } ) ) )
205 eqimss2 3231 . . . . . . . . . . . . 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 } ) ) )
206204, 205syl 15 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  ( `' ( k  e. 
NN0  |->  ( (coe1 `  a
) `  k )
) " ( _V 
\  { 0 } ) )  C_  ( `' (coe1 `  a ) "
( _V  \  {
0 } ) ) )
2079, 173mp1i 11 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e.  LMod )
20894, 195, 154, 17, 160lmod0vs 15663 . . . . . . . . . . . . 13  |-  ( ( (Poly1 ` fld )  e.  LMod  /\  x  e.  ( Base `  (Poly1 ` fld )
) )  ->  (
0 ( .s `  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
209207, 208sylan 457 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  x  e.  ( Base `  (Poly1 ` fld ) ) )  -> 
( 0 ( .s
`  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
210206, 209, 184, 193suppssov1 6075 . . . . . . . . . . 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 } ) ) )
211 ssfi 7083 . . . . . . . . . . 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 )
212201, 210, 211syl2anc 642 . . . . . . . . . 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 )
21394, 160, 164, 166, 168, 172, 199, 212gsummhm 15211 . . . . . . . . 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 ) ) ) ) ) ) )
214 eqidd 2284 . . . . . . . . . . . 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 ) ) ) ) )
21596a1i 10 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) ) )
216215feqmptd 5575 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  =  ( x  e.  ( Base `  (Poly1 ` fld )
)  |->  ( E `  x ) ) )
217 fveq2 5525 . . . . . . . . . . . 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 ) ) ) ) )
218197, 214, 216, 217fmptco 5691 . . . . . . . . . . 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 ) ) ) ) ) )
2199a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->fld  e.  Ring )
2206a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  CC  e.  _V )
22196ffvelrni 5664 . . . . . . . . . . . . . . . 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 ) ) )
222197, 221syl 15 . . . . . . . . . . . . . . 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 ) ) )
2233, 4, 67, 219, 220, 222pwselbas 13388 . . . . . . . . . . . . . 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 )
224223feqmptd 5575 . . . . . . . . . . . . 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 ) ) )
22552a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->fld  e.  CRing )
226 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  z  e.  CC )
22753, 115, 4, 54, 94, 225, 226evl1vard 19416 . . . . . . . . . . . . . . . . . 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 ) )
228188adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  k  e.  NN0 )
22953, 54, 4, 94, 225, 226, 227, 117, 128, 228evl1expd 19421 . . . . . . . . . . . . . . . . 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 ) ) )
230226, 228, 132syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^
k ) )
231230eqeq2d 2294 . . . . . . . . . . . . . . . . . 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 ) ) )
232231anbi2d 684 . . . . . . . . . . . . . . . . 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 ) ) ) )
233229, 232mpbid 201 . . . . . . . . . . . . . . . 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 ) ) )
234185adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
(coe1 `  a ) `  k )  e.  CC )
23553, 54, 4, 94, 225, 226, 233, 234, 154, 81evl1vsd 19420 . . . . . . . . . . . . . . 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
) ) ) )
236235simprd 449 . . . . . . . . . . . . . 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
) ) )
237236mpteq2dva 4106 . . . . . . . . . . . . 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 ) ) ) )
238224, 237eqtrd 2315 . . . . . . . . . . . 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
) ) ) )
239238mpteq2dva 4106 . . . . . . . . . . 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 ) ) ) ) )
240218, 239eqtrd 2315 . . . . . . . . . 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 ) ) ) ) )
241240oveq2d 5874 . . . . . . . . 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
) ) ) ) ) )
242159, 213, 2413eqtr2d 2321 . . . . . . . 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
) ) ) ) ) )
2436a1i 10 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  CC  e.  _V )
2449, 10mp1i 11 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->fld  e. CMnd )
245185adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
(coe1 `  a ) `  k )  e.  CC )
24634adantll 694 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
z ^ k )  e.  CC )
247245, 246mulcld 8855 . . . . . . . . . 10  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  x.  (
z ^ k ) )  e.  CC )
248247anasss 628 . . . . . . . . 9  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  ( z  e.  CC  /\  k  e. 
NN0 ) )  -> 
( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) )  e.  CC )
249 fzfid 11035 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin )
250 eldifn 3299 . . . . . . . . . . . . . . . . . 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 ) ) )
251250adantl 452 . . . . . . . . . . . . . . . . 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 ) ) )
252153ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 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 )
) )
253 eldifi 3298 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  ->  k  e.  NN0 )
254253adantl 452 . . . . . . . . . . . . . . . . . . . . . 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 )
255 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( deg1  ` fld )  =  ( deg1  ` fld )
256255, 54, 94, 17, 155deg1ge 19484 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0  /\  ( (coe1 `  a ) `  k
)  =/=  0 )  ->  k  <_  (
( deg1  `
fld ) `  a ) )
2572563expia 1153 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  ( ( deg1  ` fld ) `  a ) ) )
258252, 254, 257syl2anc 642 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
259 0xr 8878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
260255, 54, 94deg1xrcl 19468 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  RR* )
261153, 260syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  RR* )
262261ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 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* )
263 xrmax2 10505 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\  (
( deg1  `
fld ) `  a )  e.  RR* )  ->  (
( deg1  `
fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )
264259, 262, 263sylancr 644 . . . . . . . . . . . . . . . . . . . . . 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 ) )
265254nn0red 10019 . . . . . . . . . . . . . . . . . . . . . . . 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 )
266265rexrd 8881 . . . . . . . . . . . . . . . . . . . . . . 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* )
267 ifcl 3601 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  RR*  /\  0  e.  RR* )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
RR* )
268262, 259, 267sylancl 643 . . . . . . . . . . . . . . . . . . . . . . 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* )
269 xrletr 10489 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
270266, 262, 268, 269syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
271264, 270mpan2d 655 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
272258, 271syld 40 . . . . . . . . . . . . . . . . . . . 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 ) ) )
273272, 254jctild 527 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
274255, 54, 94deg1cl 19469 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  {  -oo } ) )
275153, 274syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  ( NN0  u.  { 
-oo } ) )
276 elun 3316 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  { 
-oo } )  <->  ( (
( deg1  `
fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  {  -oo }
) )
277275, 276sylib 188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  {  -oo }
) )
278 nn0ge0 9991 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  0  <_ 
( ( deg1  ` fld ) `  a ) )
279 iftrue 3571 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  <_  ( ( deg1  ` fld ) `  a )  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  ( ( deg1  ` fld ) `  a ) )
280278, 279syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  ( ( deg1  ` fld ) `  a ) )
281 id 19 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  ( ( deg1  ` fld ) `
 a )  e. 
NN0 )
282280, 281eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
283 0re 8838 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  e.  RR
284 mnflt 10464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  e.  RR  ->  -oo  <  0 )
285283, 284ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  -oo  <  0
286 mnfxr 10456 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  -oo  e.  RR*
287 xrltnle 8891 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 
-oo  e.  RR*  /\  0  e.  RR* )  ->  (  -oo  <  0  <->  -.  0  <_  -oo ) )
288286, 259, 287mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  (  -oo  <  0  <->  -.  0  <_  -oo )
289285, 288mpbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -.  0  <_  -oo
290 elsni 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  ( ( deg1  ` fld ) `  a )  =  -oo )
291290breq2d 4035 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  ( 0  <_  (
( deg1  `
fld ) `  a )  <->  0  <_  -oo ) )
292289, 291mtbiri 294 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  -.  0  <_  (
( deg1  `
fld ) `  a ) )
293 iffalse 3572 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  0  <_  ( ( deg1  ` fld ) `  a )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  0 )
294292, 293syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  0 )
295 0nn0 9980 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  NN0
296294, 295syl6eqel 2371 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  {  -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
297282, 296jaoi 368 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  {  -oo }
)  ->  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
298277, 297syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
299298ad2antrr 706 . . . . . . . . . . . . . . . . . . . 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 )
300 fznn0 10851 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
301299, 300syl 15 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
302273, 301sylibrd 225 . . . . . . . . . . . . . . . . . 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 ) ) ) )
303302necon1bd 2514 . . . . . . . . . . . . . . . . 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 ) )
304251, 303mpd 14 . . . . . . . . . . . . . . . 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 )
305304oveq1d 5873 . . . . . . . . . . . . . . 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 ) ) )
306253, 246sylan2 460 . . . . . . . . . . . . . . . 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 )
307306mul02d 9010 . . . . . . . . . . . . . . 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 )
308305, 307eqtrd 2315 . . . . . . . . . . . . . 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 )
309308an32s 779 . . . . . . . . . . . . 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 )
310309mpteq2dva 4106 . . . . . . . . . . . 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 ) )
311 fconstmpt 4732 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( z  e.  CC  |->  0 )
312 rngmnd 15350 . . . . . . . . . . . . . . 15  |-  (fld  e.  Ring  ->fld  e.  Mnd )
3139, 312ax-mp 8 . . . . . . . . . . . . . 14  |-fld  e.  Mnd
3143, 17pws0g 14408 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Mnd  /\  CC  e.  _V )  ->  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) ) )
315313, 6, 314mp2an 653 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) )
316311, 315eqtr3i 2305 . . . . . . . . . . . 12  |-  ( z  e.  CC  |->  0 )  =  ( 0g `  (fld  ^s  CC ) )
317310, 316syl6eq 2331 . . . . . . . . . . 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 ) ) )
318317suppss2 6073 . . . . . . . . . 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 ) ) )
319 ssfi 7083 . . . . . . . . . 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 )
320249, 318, 319syl2anc 642 . . . . . . . . 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 )
3213, 4, 5, 243, 168, 244, 248, 320pwsgsum 15230 . . . . . . . 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
) ) ) ) ) )
322 elfznn0 10822 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  ->  k  e.  NN0 )
323322ssriv 3184 . . . . . . . . . . . 12  |-  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
C_  NN0
324 resmpt 5000 . . . . . . . . . . . 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
) ) ) )
325323, 324ax-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
) ) )
326325oveq2i 5869 . . . . . . . . . 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
) ) ) )
3279, 10mp1i 11 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->fld  e. CMnd )
328167a1i 10 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->  NN0  e.  _V )
329 eqid 2283 . . . . . . . . . . . 12  |-  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )  =  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )
330247, 329fmptd 5684 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  z  e.  CC )  ->  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) : NN0 --> CC )
331308suppss2 6073 . . . . . . . . . . 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 ) ,  (