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

Theorem plypf1 21649
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 21632 . . . . 5  |-  ( f  e.  (Poly `  S
)  <->  ( S  C_  CC  /\  E. n  e. 
NN0  E. a  e.  ( ( S  u.  {
0 } )  ^m  NN0 ) f  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... n ) ( ( a `  k
)  x.  ( z ^ k ) ) ) ) )
21simprbi 464 . . . 4  |-  ( f  e.  (Poly `  S
)  ->  E. n  e.  NN0  E. a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) f  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... n ) ( ( a `  k
)  x.  ( z ^ k ) ) ) )
3 eqid 2437 . . . . . . . . 9  |-  (fld  ^s  CC )  =  (fld 
^s 
CC )
4 cnfldbas 17791 . . . . . . . . 9  |-  CC  =  ( Base ` fld )
5 eqid 2437 . . . . . . . . 9  |-  ( 0g
`  (fld 
^s 
CC ) )  =  ( 0g `  (fld  ^s  CC ) )
6 cnex 9355 . . . . . . . . . 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 11787 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( 0 ... n
)  e.  Fin )
9 cnrng 17807 . . . . . . . . . 10  |-fld  e.  Ring
10 rngcmn 16661 . . . . . . . . . 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 16842 . . . . . . . . . . . . 13  |-  ( S  e.  (SubRing ` fld )  ->  S  C_  CC )
1312ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  S  C_  CC )
14 elmapi 7226 . . . . . . . . . . . . . . 15  |-  ( a  e.  ( ( S  u.  { 0 } )  ^m  NN0 )  ->  a : NN0 --> ( S  u.  { 0 } ) )
1514ad2antll 728 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> ( S  u.  { 0 } ) )
16 subrgsubg 16847 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubRing ` fld )  ->  S  e.  (SubGrp ` fld ) )
17 cnfld0 17809 . . . . . . . . . . . . . . . . . . . 20  |-  0  =  ( 0g ` fld )
1817subg0cl 15678 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  (SubGrp ` fld )  ->  0  e.  S )
1916, 18syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( S  e.  (SubRing ` fld )  ->  0  e.  S )
2019adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
0  e.  S )
2120snssd 4011 . . . . . . . . . . . . . . . 16  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  { 0 }  C_  S )
22 ssequn2 3522 . . . . . . . . . . . . . . . 16  |-  ( { 0 }  C_  S  <->  ( S  u.  { 0 } )  =  S )
2321, 22sylib 196 . . . . . . . . . . . . . . 15  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( S  u.  {
0 } )  =  S )
24 feq3 5537 . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
a : NN0 --> S )
27 elfznn0 11473 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... n )  ->  k  e.  NN0 )
28 ffvelrn 5834 . . . . . . . . . . . . 13  |-  ( ( a : NN0 --> S  /\  k  e.  NN0 )  -> 
( a `  k
)  e.  S )
2926, 27, 28syl2an 477 . . . . . . . . . . . 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 3350 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( a `  k )  e.  CC )
3130adantrl 715 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  ( z  e.  CC  /\  k  e.  ( 0 ... n ) ) )  ->  ( a `  k )  e.  CC )
32 simprl 755 . . . . . . . . . . 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 728 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  ( z  e.  CC  /\  k  e.  ( 0 ... n ) ) )  ->  k  e.  NN0 )
34 expcl 11875 . . . . . . . . . . 11  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( z ^ k
)  e.  CC )
3532, 33, 34syl2anc 661 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  ( z  e.  CC  /\  k  e.  ( 0 ... n ) ) )  ->  ( z ^ k )  e.  CC )
3631, 35mulcld 9398 . . . . . . . . 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 )
37 eqid 2437 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... n )  |->  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) ) )  =  ( k  e.  ( 0 ... n )  |->  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) ) )
386mptex 5941 . . . . . . . . . . 11  |-  ( z  e.  CC  |->  ( ( a `  k )  x.  ( z ^
k ) ) )  e.  _V
3938a1i 11 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( z  e.  CC  |->  ( ( a `
 k )  x.  ( z ^ k
) ) )  e. 
_V )
40 fvex 5694 . . . . . . . . . . 11  |-  ( 0g
`  (fld 
^s 
CC ) )  e. 
_V
4140a1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( 0g `  (fld  ^s  CC ) )  e.  _V )
4237, 8, 39, 41fsuppmptdm 7623 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( k  e.  ( 0 ... n ) 
|->  ( z  e.  CC  |->  ( ( a `  k )  x.  (
z ^ k ) ) ) ) finSupp  ( 0g `  (fld 
^s 
CC ) ) )
433, 4, 5, 7, 8, 11, 36, 42pwsgsum 16459 . . . . . . . 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 ) ) ) ) ) )
44 fzfid 11787 . . . . . . . . . 10  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  z  e.  CC )  ->  ( 0 ... n
)  e.  Fin )
4536anassrs 648 . . . . . . . . . 10  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  z  e.  CC )  /\  k  e.  (
0 ... n ) )  ->  ( ( a `
 k )  x.  ( z ^ k
) )  e.  CC )
4644, 45gsumfsum 17848 . . . . . . . . 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 ) ) )
4746mpteq2dva 4371 . . . . . . . 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 ) ) ) )
4843, 47eqtrd 2469 . . . . . . 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 ) ) ) )
493pwsrng 16693 . . . . . . . . . 10  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  (fld 
^s 
CC )  e.  Ring )
509, 6, 49mp2an 672 . . . . . . . . 9  |-  (fld  ^s  CC )  e.  Ring
51 rngcmn 16661 . . . . . . . . 9  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e. CMnd )
5250, 51mp1i 12 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
(fld  ^s  CC )  e. CMnd )
53 cncrng 17806 . . . . . . . . . . 11  |-fld  e.  CRing
54 plypf1.e . . . . . . . . . . . 12  |-  E  =  (eval1 ` fld )
55 eqid 2437 . . . . . . . . . . . 12  |-  (Poly1 ` fld )  =  (Poly1 ` fld )
5654, 55, 3, 4evl1rhm 17735 . . . . . . . . . . 11  |-  (fld  e.  CRing  ->  E  e.  ( (Poly1 ` fld ) RingHom  (fld  ^s  CC ) ) )
5753, 56ax-mp 5 . . . . . . . . . 10  |-  E  e.  ( (Poly1 ` fld ) RingHom  (fld 
^s 
CC ) )
58 plypf1.r . . . . . . . . . . . 12  |-  R  =  (flds  S )
59 plypf1.p . . . . . . . . . . . 12  |-  P  =  (Poly1 `  R )
60 plypf1.a . . . . . . . . . . . 12  |-  A  =  ( Base `  P
)
6155, 58, 59, 60subrgply1 17659 . . . . . . . . . . 11  |-  ( S  e.  (SubRing ` fld )  ->  A  e.  (SubRing `  (Poly1 ` fld ) ) )
6261adantr 465 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  ->  A  e.  (SubRing `  (Poly1 ` fld )
) )
63 rhmima 16872 . . . . . . . . . 10  |-  ( ( E  e.  ( (Poly1 ` fld ) RingHom 
(fld  ^s  CC ) )  /\  A  e.  (SubRing `  (Poly1 ` fld ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
6457, 62, 63sylancr 663 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubRing `  (fld  ^s  CC ) ) )
65 subrgsubg 16847 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubGrp `  (fld 
^s 
CC ) ) )
66 subgsubm 15692 . . . . . . . . 9  |-  ( ( E " A )  e.  (SubGrp `  (fld  ^s  CC ) )  ->  ( E " A )  e.  (SubMnd `  (fld 
^s 
CC ) ) )
6764, 65, 663syl 20 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( E " A
)  e.  (SubMnd `  (fld  ^s  CC ) ) )
68 eqid 2437 . . . . . . . . . . . 12  |-  ( Base `  (fld 
^s 
CC ) )  =  ( Base `  (fld  ^s  CC ) )
699a1i 11 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->fld 
e.  Ring )
706a1i 11 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  CC  e.  _V )
71 fconst6g 5592 . . . . . . . . . . . . . 14  |-  ( ( a `  k )  e.  CC  ->  ( CC  X.  { ( a `
 k ) } ) : CC --> CC )
7230, 71syl 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 )
733, 4, 68pwselbasb 14418 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  ( ( CC 
X.  { ( a `
 k ) } )  e.  ( Base `  (fld 
^s 
CC ) )  <->  ( CC  X.  { ( a `  k ) } ) : CC --> CC ) )
749, 6, 73mp2an 672 . . . . . . . . . . . . 13  |-  ( ( CC  X.  { ( a `  k ) } )  e.  (
Base `  (fld  ^s  CC )
)  <->  ( CC  X.  { ( a `  k ) } ) : CC --> CC )
7572, 74sylibr 212 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( CC  X.  { ( a `  k ) } )  e.  ( Base `  (fld  ^s  CC ) ) )
7635anass1rs 805 . . . . . . . . . . . . . 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 )
77 eqid 2437 . . . . . . . . . . . . . 14  |-  ( z  e.  CC  |->  ( z ^ k ) )  =  ( z  e.  CC  |->  ( z ^
k ) )
7876, 77fmptd 5860 . . . . . . . . . . . . 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 )
793, 4, 68pwselbasb 14418 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Ring  /\  CC  e.  _V )  ->  ( ( z  e.  CC  |->  ( z ^ k ) )  e.  ( Base `  (fld  ^s  CC ) )  <->  ( z  e.  CC  |->  ( z ^
k ) ) : CC --> CC ) )
809, 6, 79mp2an 672 . . . . . . . . . . . . 13  |-  ( ( z  e.  CC  |->  ( z ^ k ) )  e.  ( Base `  (fld 
^s 
CC ) )  <->  ( z  e.  CC  |->  ( z ^
k ) ) : CC --> CC )
8178, 80sylibr 212 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( z  e.  CC  |->  ( z ^
k ) )  e.  ( Base `  (fld  ^s  CC ) ) )
82 cnfldmul 17793 . . . . . . . . . . . 12  |-  x.  =  ( .r ` fld )
83 eqid 2437 . . . . . . . . . . . 12  |-  ( .r
`  (fld 
^s 
CC ) )  =  ( .r `  (fld  ^s  CC ) )
843, 68, 69, 70, 75, 81, 82, 83pwsmulrval 14421 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( ( CC 
X.  { ( a `
 k ) } ) ( .r `  (fld  ^s  CC ) ) ( z  e.  CC  |->  ( z ^ k ) ) )  =  ( ( CC  X.  { ( a `  k ) } )  oF  x.  ( z  e.  CC  |->  ( z ^
k ) ) ) )
8530adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( a `  k )  e.  CC )
86 fconstmpt 4874 . . . . . . . . . . . . 13  |-  ( CC 
X.  { ( a `
 k ) } )  =  ( z  e.  CC  |->  ( a `
 k ) )
8786a1i 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 ) ) )
88 eqidd 2438 . . . . . . . . . . . 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
) ) )
8970, 85, 76, 87, 88offval2 6331 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( ( CC 
X.  { ( a `
 k ) } )  oF  x.  ( z  e.  CC  |->  ( z ^ k
) ) )  =  ( z  e.  CC  |->  ( ( a `  k )  x.  (
z ^ k ) ) ) )
9084, 89eqtrd 2469 . . . . . . . . . 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 ) ) ) )
9164adantr 465 . . . . . . . . . . 11  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E " A )  e.  (SubRing `  (fld 
^s 
CC ) ) )
92 eqid 2437 . . . . . . . . . . . . . 14  |-  (algSc `  (Poly1 ` fld ) )  =  (algSc `  (Poly1 ` fld ) )
9354, 55, 4, 92evl1sca 17737 . . . . . . . . . . . . 13  |-  ( (fld  e. 
CRing  /\  ( a `  k )  e.  CC )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  =  ( CC  X.  { ( a `  k ) } ) )
9453, 30, 93sylancr 663 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( E `  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
) )  =  ( CC  X.  { ( a `  k ) } ) )
95 eqid 2437 . . . . . . . . . . . . . . . 16  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (Poly1 ` fld ) )
9695, 68rhmf 16800 . . . . . . . . . . . . . . 15  |-  ( E  e.  ( (Poly1 ` fld ) RingHom  (fld 
^s 
CC ) )  ->  E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) ) )
9757, 96ax-mp 5 . . . . . . . . . . . . . 14  |-  E :
( Base `  (Poly1 ` fld ) ) --> ( Base `  (fld 
^s 
CC ) )
98 ffn 5552 . . . . . . . . . . . . . 14  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  E  Fn  ( Base `  (Poly1 ` fld ) ) )
9997, 98mp1i 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 ) ) )
10095subrgss 16842 . . . . . . . . . . . . . . 15  |-  ( A  e.  (SubRing `  (Poly1 ` fld )
)  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
10161, 100syl 16 . . . . . . . . . . . . . 14  |-  ( S  e.  (SubRing ` fld )  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
102101ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  A  C_  ( Base `  (Poly1 ` fld ) ) )
103 simpll 753 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  S  e.  (SubRing ` fld ) )
10455, 92, 58, 59, 103, 60, 4, 30subrg1asclcl 17685 . . . . . . . . . . . . . 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
) )
10529, 104mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  ( (algSc `  (Poly1 ` fld ) ) `  (
a `  k )
)  e.  A )
106 fnfvima 5948 . . . . . . . . . . . . 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 ) )
10799, 102, 105, 106syl3anc 1218 . . . . . . . . . . . 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 ) )
10894, 107eqeltrrd 2512 . . . . . . . . . . 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 ) )
10968subrgss 16842 . . . . . . . . . . . . . . . . 17  |-  ( ( E " A )  e.  (SubRing `  (fld  ^s  CC ) )  ->  ( E " A )  C_  ( Base `  (fld 
^s 
CC ) ) )
11091, 109syl 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 ) ) )
11161ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  A  e.  (SubRing `  (Poly1 ` fld ) ) )
112 eqid 2437 . . . . . . . . . . . . . . . . . . . 20  |-  (mulGrp `  (Poly1 ` fld ) )  =  (mulGrp `  (Poly1 ` fld ) )
113112subrgsubm 16854 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  (SubRing `  (Poly1 ` fld )
)  ->  A  e.  (SubMnd `  (mulGrp `  (Poly1 ` fld )
) ) )
114111, 113syl 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 ) ) ) )
11527adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  k  e.  NN0 )
116 eqid 2437 . . . . . . . . . . . . . . . . . . 19  |-  (var1 ` fld )  =  (var1 ` fld )
117116, 103, 58, 59, 60subrgvr1cl 17687 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( S  e.  (SubRing ` fld )  /\  ( n  e. 
NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  ->  (var1 ` fld )  e.  A )
118 eqid 2437 . . . . . . . . . . . . . . . . . . 19  |-  (.g `  (mulGrp `  (Poly1 ` fld ) ) )  =  (.g `  (mulGrp `  (Poly1 ` fld )
) )
119118submmulgcl 15650 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  (SubMnd `  (mulGrp `  (Poly1 ` fld ) ) )  /\  k  e.  NN0  /\  (var1 ` fld )  e.  A )  ->  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  A
)
120114, 115, 117, 119syl3anc 1218 . . . . . . . . . . . . . . . . 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 )
121 fnfvima 5948 . . . . . . . . . . . . . . . . 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 ) )
12299, 102, 120, 121syl3anc 1218 . . . . . . . . . . . . . . . 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 ) )
123110, 122sseldd 3350 . . . . . . . . . . . . . . 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 )
) )
1243, 4, 68, 69, 70, 123pwselbas 14419 . . . . . . . . . . . . . 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 )
125124feqmptd 5737 . . . . . . . . . . . . 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 ) ) )
12653a1i 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 )
127 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  z  e.  CC )
12854, 116, 4, 55, 95, 126, 127evl1vard 17740 . . . . . . . . . . . . . . . . 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 ) )
129 eqid 2437 . . . . . . . . . . . . . . . . 17  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
130115adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  k  e.  NN0 )
13154, 55, 4, 95, 126, 127, 128, 118, 129, 130evl1expd 17748 . . . . . . . . . . . . . . . 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 ) ) )
132131simprd 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( ( E `
 ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) `  z
)  =  ( k (.g `  (mulGrp ` fld ) ) z ) )
133 cnfldexp 17818 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  CC  /\  k  e.  NN0 )  -> 
( k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^ k
) )
134127, 130, 133syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  /\  k  e.  ( 0 ... n ) )  /\  z  e.  CC )  ->  ( k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^
k ) )
135132, 134eqtrd 2469 . . . . . . . . . . . . . 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 ) )
136135mpteq2dva 4371 . . . . . . . . . . . . 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 ) ) )
137125, 136eqtrd 2469 . . . . . . . . . . . 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 ) ) )
138137, 122eqeltrrd 2512 . . . . . . . . . . 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
) )
13983subrgmcl 16853 . . . . . . . . . . 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 ) )
14091, 108, 138, 139syl3anc 1218 . . . . . . . . . 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 ) )
14190, 140eqeltrrd 2512 . . . . . . . . 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
) )
142141, 37fmptd 5860 . . . . . . . 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 ) )
14337, 8, 141, 41fsuppmptdm 7623 . . . . . . . 8  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( k  e.  ( 0 ... n ) 
|->  ( z  e.  CC  |->  ( ( a `  k )  x.  (
z ^ k ) ) ) ) finSupp  ( 0g `  (fld 
^s 
CC ) ) )
1445, 52, 8, 67, 142, 143gsumsubmcl 16393 . . . . . . 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 ) )
14548, 144eqeltrrd 2512 . . . . . 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 ) )
146 eleq1 2497 . . . . . 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 ) ) )
147145, 146syl5ibrcom 222 . . . . 5  |-  ( ( S  e.  (SubRing ` fld )  /\  (
n  e.  NN0  /\  a  e.  ( ( S  u.  { 0 } )  ^m  NN0 ) ) )  -> 
( f  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... n ) ( ( a `  k
)  x.  ( z ^ k ) ) )  ->  f  e.  ( E " A ) ) )
148147rexlimdvva 2842 . . . 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 ) ) )
1492, 148syl5 32 . . 3  |-  ( S  e.  (SubRing ` fld )  ->  ( f  e.  (Poly `  S
)  ->  f  e.  ( E " A ) ) )
150 ffun 5554 . . . . . 6  |-  ( E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) )  ->  Fun  E )
15197, 150ax-mp 5 . . . . 5  |-  Fun  E
152 fvelima 5736 . . . . 5  |-  ( ( Fun  E  /\  f  e.  ( E " A
) )  ->  E. a  e.  A  ( E `  a )  =  f )
153151, 152mpan 670 . . . 4  |-  ( f  e.  ( E " A )  ->  E. a  e.  A  ( E `  a )  =  f )
154101sselda 3349 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  a  e.  ( Base `  (Poly1 ` fld )
) )
155 eqid 2437 . . . . . . . . . . . 12  |-  ( .s
`  (Poly1 ` fld ) )  =  ( .s `  (Poly1 ` fld ) )
156 eqid 2437 . . . . . . . . . . . 12  |-  (coe1 `  a
)  =  (coe1 `  a
)
157 cnfldex 17790 . . . . . . . . . . . 12  |-fld  e.  _V
15855, 116, 95, 155, 112, 118, 156, 157ply1coe 17716 . . . . . . . . . . 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 ) ) ) ) ) )
15953, 154, 158sylancr 663 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  a  =  ( (Poly1 ` fld )  gsumg  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) ) )
160159fveq2d 5688 . . . . . . . . 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 ) ) ) ) ) ) )
161 eqid 2437 . . . . . . . . . 10  |-  ( 0g
`  (Poly1 ` fld ) )  =  ( 0g `  (Poly1 ` fld ) )
16255ply1rng 17674 . . . . . . . . . . . 12  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  Ring )
1639, 162ax-mp 5 . . . . . . . . . . 11  |-  (Poly1 ` fld )  e.  Ring
164 rngcmn 16661 . . . . . . . . . . 11  |-  ( (Poly1 ` fld )  e.  Ring  ->  (Poly1 ` fld )  e. CMnd )
165163, 164mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e. CMnd )
166 rngmnd 16640 . . . . . . . . . . 11  |-  ( (fld  ^s  CC )  e.  Ring  ->  (fld  ^s  CC )  e.  Mnd )
16750, 166mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (fld  ^s  CC )  e.  Mnd )
168 nn0ex 10577 . . . . . . . . . . 11  |-  NN0  e.  _V
169168a1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  NN0  e.  _V )
170 rhmghm 16799 . . . . . . . . . . . 12  |-  ( E  e.  ( (Poly1 ` fld ) RingHom  (fld 
^s 
CC ) )  ->  E  e.  ( (Poly1 ` fld )  GrpHom  (fld 
^s 
CC ) ) )
17157, 170ax-mp 5 . . . . . . . . . . 11  |-  E  e.  ( (Poly1 ` fld )  GrpHom  (fld 
^s 
CC ) )
172 ghmmhm 15746 . . . . . . . . . . 11  |-  ( E  e.  ( (Poly1 ` fld )  GrpHom  (fld  ^s  CC ) )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
173171, 172mp1i 12 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  e.  ( (Poly1 ` fld ) MndHom  (fld 
^s 
CC ) ) )
17455ply1lmod 17678 . . . . . . . . . . . . 13  |-  (fld  e.  Ring  -> 
(Poly1 `
fld )  e.  LMod )
1759, 174mp1i 12 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (Poly1 ` fld )  e.  LMod )
17612ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  S  C_  CC )
177 eqid 2437 . . . . . . . . . . . . . . . . 17  |-  ( Base `  R )  =  (
Base `  R )
178156, 60, 59, 177coe1f 17639 . . . . . . . . . . . . . . . 16  |-  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> (
Base `  R )
)
17958subrgbas 16850 . . . . . . . . . . . . . . . . 17  |-  ( S  e.  (SubRing ` fld )  ->  S  =  ( Base `  R
) )
180 feq3 5537 . . . . . . . . . . . . . . . . 17  |-  ( S  =  ( Base `  R
)  ->  ( (coe1 `  a ) : NN0 --> S  <-> 
(coe1 `  a ) : NN0 --> ( Base `  R
) ) )
181179, 180syl 16 . . . . . . . . . . . . . . . 16  |-  ( S  e.  (SubRing ` fld )  ->  ( (coe1 `  a ) : NN0 --> S  <-> 
(coe1 `  a ) : NN0 --> ( Base `  R
) ) )
182178, 181syl5ibr 221 . . . . . . . . . . . . . . 15  |-  ( S  e.  (SubRing ` fld )  ->  ( a  e.  A  ->  (coe1 `  a ) : NN0 --> S ) )
183182imp 429 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a ) : NN0 --> S )
184183ffvelrnda 5836 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  S )
185176, 184sseldd 3350 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( (coe1 `  a ) `  k
)  e.  CC )
186112rngmgp 16637 . . . . . . . . . . . . . 14  |-  ( (Poly1 ` fld )  e.  Ring  ->  (mulGrp `  (Poly1 ` fld ) )  e.  Mnd )
187163, 186mp1i 12 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (mulGrp `  (Poly1 ` fld )
)  e.  Mnd )
188 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  k  e.  NN0 )
189116, 55, 95vr1cl 17643 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  -> 
(var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
1909, 189mp1i 12 . . . . . . . . . . . . 13  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  (var1 ` fld )  e.  ( Base `  (Poly1 ` fld ) ) )
191112, 95mgpbas 16583 . . . . . . . . . . . . . 14  |-  ( Base `  (Poly1 ` fld ) )  =  (
Base `  (mulGrp `  (Poly1 ` fld )
) )
192191, 118mulgnn0cl 15632 . . . . . . . . . . . . 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 1218 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  ( k
(.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  (
Base `  (Poly1 ` fld ) ) )
19455ply1sca 17679 . . . . . . . . . . . . . 14  |-  (fld  e.  Ring  ->fld  =  (Scalar `  (Poly1 ` fld ) ) )
1959, 194ax-mp 5 . . . . . . . . . . . . 13  |-fld  =  (Scalar `  (Poly1 ` fld )
)
19695, 195, 155, 4lmodvscl 16941 . . . . . . . . . . . 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 ) ) )
197175, 185, 193, 196syl3anc 1218 . . . . . . . . . . 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 2437 . . . . . . . . . . 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 5860 . . . . . . . . . 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 ) ) )
200168mptex 5941 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  e.  _V
201 funmpt 5447 . . . . . . . . . . . . 13  |-  Fun  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )
202 fvex 5694 . . . . . . . . . . . . 13  |-  ( 0g
`  (Poly1 ` fld ) )  e.  _V
203200, 201, 2023pm3.2i 1166 . . . . . . . . . . . 12  |-  ( ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  e.  _V  /\  Fun  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  /\  ( 0g `  (Poly1 ` fld ) )  e.  _V )
204203a1i 11 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  e. 
_V  /\  Fun  ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  /\  ( 0g `  (Poly1 ` fld ) )  e.  _V ) )
205156, 95, 55, 17coe1sfi 17640 . . . . . . . . . . . . 13  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  (coe1 `  a
) finSupp  0 )
206154, 205syl 16 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a ) finSupp  0 )
207206fsuppimpd 7619 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(coe1 `  a ) supp  0
)  e.  Fin )
208183feqmptd 5737 . . . . . . . . . . . . . 14  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (coe1 `  a )  =  ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) )
209208oveq1d 6101 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
(coe1 `  a ) supp  0
)  =  ( ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) supp  0 ) )
210 eqimss2 3402 . . . . . . . . . . . . 13  |-  ( ( (coe1 `  a ) supp  0
)  =  ( ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) supp  0 )  ->  ( ( k  e.  NN0  |->  ( (coe1 `  a ) `  k
) ) supp  0 ) 
C_  ( (coe1 `  a
) supp  0 ) )
211209, 210syl 16 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( (coe1 `  a ) `  k ) ) supp  0
)  C_  ( (coe1 `  a ) supp  0 ) )
2129, 174mp1i 12 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (Poly1 ` fld )  e.  LMod )
21395, 195, 155, 17, 161lmod0vs 16957 . . . . . . . . . . . . 13  |-  ( ( (Poly1 ` fld )  e.  LMod  /\  x  e.  ( Base `  (Poly1 ` fld )
) )  ->  (
0 ( .s `  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
214212, 213sylan 471 . . . . . . . . . . . 12  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  x  e.  ( Base `  (Poly1 ` fld ) ) )  -> 
( 0 ( .s
`  (Poly1 ` fld ) ) x )  =  ( 0g `  (Poly1 ` fld ) ) )
215 c0ex 9372 . . . . . . . . . . . . 13  |-  0  e.  _V
216215a1i 11 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  0  e.  _V )
217211, 214, 184, 193, 216suppssov1 6716 . . . . . . . . . . 11  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) supp  ( 0g `  (Poly1 ` fld ) ) )  C_  ( (coe1 `  a ) supp  0
) )
218 suppssfifsupp 7627 . . . . . . . . . . 11  |-  ( ( ( ( k  e. 
NN0  |->  ( ( (coe1 `  a ) `  k
) ( .s `  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) )  e.  _V  /\  Fun  ( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) )  /\  ( 0g `  (Poly1 ` fld ) )  e.  _V )  /\  ( ( (coe1 `  a ) supp  0 )  e.  Fin  /\  (
( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) supp  ( 0g `  (Poly1 ` fld ) ) )  C_  ( (coe1 `  a ) supp  0
) ) )  -> 
( k  e.  NN0  |->  ( ( (coe1 `  a
) `  k )
( .s `  (Poly1 ` fld )
) ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) ) ) ) finSupp  ( 0g `  (Poly1 ` fld ) ) )
219204, 207, 217, 218syl12anc 1216 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
k  e.  NN0  |->  ( ( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) finSupp 
( 0g `  (Poly1 ` fld )
) )
22095, 161, 165, 167, 169, 173, 199, 219gsummhm 16420 . . . . . . . . 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 ) ) ) ) ) ) )
221 eqidd 2438 . . . . . . . . . . . 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 ) ) ) ) )
22297a1i 11 . . . . . . . . . . . . 13  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E : ( Base `  (Poly1 ` fld )
) --> ( Base `  (fld  ^s  CC ) ) )
223222feqmptd 5737 . . . . . . . . . . . 12  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  E  =  ( x  e.  ( Base `  (Poly1 ` fld )
)  |->  ( E `  x ) ) )
224 fveq2 5684 . . . . . . . . . . . 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 ) ) ) ) )
225197, 221, 223, 224fmptco 5869 . . . . . . . . . . 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 ) ) ) ) ) )
2269a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->fld  e.  Ring )
2276a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  k  e.  NN0 )  ->  CC  e.  _V )
22897ffvelrni 5835 . . . . . . . . . . . . . . . 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 ) ) )
229197, 228syl 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 ) ) )
2303, 4, 68, 226, 227, 229pwselbas 14419 . . . . . . . . . . . . . 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 )
231230feqmptd 5737 . . . . . . . . . . . . 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 ) ) )
23253a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->fld  e.  CRing )
233 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  z  e.  CC )
23454, 116, 4, 55, 95, 232, 233evl1vard 17740 . . . . . . . . . . . . . . . . . 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 ) )
235188adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  k  e.  NN0 )
23654, 55, 4, 95, 232, 233, 234, 118, 129, 235evl1expd 17748 . . . . . . . . . . . . . . . . 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 ) ) )
237233, 235, 133syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
k (.g `  (mulGrp ` fld ) ) z )  =  ( z ^
k ) )
238237eqeq2d 2448 . . . . . . . . . . . . . . . . . 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 ) ) )
239238anbi2d 703 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( ( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) )  e.  ( Base `  (Poly1 ` fld ) )  /\  (
( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z )  =  ( k (.g `  (mulGrp ` fld ) ) z ) )  <->  ( ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) )  e.  (
Base `  (Poly1 ` fld ) )  /\  (
( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z )  =  ( z ^ k ) ) ) )
240236, 239mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( k (.g `  (mulGrp `  (Poly1 ` fld ) ) ) (var1 ` fld ) )  e.  ( Base `  (Poly1 ` fld ) )  /\  (
( E `  (
k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) `  z )  =  ( z ^ k ) ) )
241185adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
(coe1 `  a ) `  k )  e.  CC )
24254, 55, 4, 95, 232, 233, 240, 241, 155, 82evl1vsd 17747 . . . . . . . . . . . . . . 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
) ) ) )
243242simprd 463 . . . . . . . . . . . . . 14  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  k  e.  NN0 )  /\  z  e.  CC )  ->  (
( E `  (
( (coe1 `  a ) `  k ) ( .s
`  (Poly1 ` fld ) ) ( k (.g `  (mulGrp `  (Poly1 ` fld )
) ) (var1 ` fld ) ) ) ) `
 z )  =  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) )
244243mpteq2dva 4371 . . . . . . . . . . . . 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 ) ) ) )
245231, 244eqtrd 2469 . . . . . . . . . . . 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
) ) ) )
246245mpteq2dva 4371 . . . . . . . . . . 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 ) ) ) ) )
247225, 246eqtrd 2469 . . . . . . . . . 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 ) ) ) ) )
248247oveq2d 6102 . . . . . . . . 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
) ) ) ) ) )
249160, 220, 2483eqtr2d 2475 . . . . . . . 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
) ) ) ) ) )
2506a1i 11 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  CC  e.  _V )
2519, 10mp1i 12 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->fld  e. CMnd )
252185adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
(coe1 `  a ) `  k )  e.  CC )
25334adantll 713 . . . . . . . . . . 11  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
z ^ k )  e.  CC )
254252, 253mulcld 9398 . . . . . . . . . 10  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  x.  (
z ^ k ) )  e.  CC )
255254anasss 647 . . . . . . . . 9  |-  ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A
)  /\  ( z  e.  CC  /\  k  e. 
NN0 ) )  -> 
( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) )  e.  CC )
256168mptex 5941 . . . . . . . . . . . 12  |-  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) )  e. 
_V
257 funmpt 5447 . . . . . . . . . . . 12  |-  Fun  (
k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) )
258256, 257, 403pm3.2i 1166 . . . . . . . . . . 11  |-  ( ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) )  e. 
_V  /\  Fun  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) )  /\  ( 0g `  (fld  ^s  CC ) )  e.  _V )
259258a1i 11 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) )  e.  _V  /\  Fun  ( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) )  /\  ( 0g `  (fld  ^s  CC ) )  e.  _V ) )
260 fzfid 11787 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin )
261 eldifn 3472 . . . . . . . . . . . . . . . . . 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 ) ) )
262261adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  -.  k  e.  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
263154ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  a  e.  ( Base `  (Poly1 ` fld )
) )
264 eldifi 3471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  ->  k  e.  NN0 )
265264adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  k  e.  NN0 )
266 eqid 2437 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( deg1  ` fld )  =  ( deg1  ` fld )
267266, 55, 95, 17, 156deg1ge 21539 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0  /\  ( (coe1 `  a ) `  k
)  =/=  0 )  ->  k  <_  (
( deg1  `
fld ) `  a ) )
2682673expia 1189 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  ( Base `  (Poly1 ` fld ) )  /\  k  e.  NN0 )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  ( ( deg1  ` fld ) `  a ) ) )
269263, 265, 268syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  ( ( deg1  ` fld ) `  a ) ) )
270 0xr 9422 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  RR*
271266, 55, 95deg1xrcl 21522 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  RR* )
272154, 271syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  RR* )
273272ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( deg1  `
fld ) `  a )  e.  RR* )
274 xrmax2 11140 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 0  e.  RR*  /\  (
( deg1  `
fld ) `  a )  e.  RR* )  ->  (
( deg1  `
fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )
275270, 273, 274sylancr 663 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( deg1  `
fld ) `  a )  <_  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )
276265nn0red 10629 . . . . . . . . . . . . . . . . . . . . . . . 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 )
277276rexrd 9425 . . . . . . . . . . . . . . . . . . . . . . 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* )
278 ifcl 3824 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  RR*  /\  0  e.  RR* )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
RR* )
279273, 270, 278sylancl 662 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
RR* )
280 xrletr 11124 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
281277, 273, 279, 280syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
282275, 281mpan2d 674 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
k  <_  ( ( deg1  ` fld ) `  a )  ->  k  <_  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
283269, 282syld 44 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  <_  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
284283, 265jctild 543 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  ( k  e.  NN0  /\  k  <_  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )
285266, 55, 95deg1cl 21523 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  ( Base `  (Poly1 ` fld )
)  ->  ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  { -oo } ) )
286154, 285syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( deg1  `
fld ) `  a )  e.  ( NN0  u.  { -oo } ) )
287 elun 3490 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  ( NN0  u.  { -oo } )  <->  ( (
( deg1  `
fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
) )
288286, 287sylib 196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
) )
289 nn0ge0 10597 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  0  <_ 
( ( deg1  ` fld ) `  a ) )
290 iftrue 3790 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  <_  ( ( deg1  ` fld ) `  a )  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  ( ( deg1  ` fld ) `  a ) )
291289, 290syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  ( ( deg1  ` fld ) `  a ) )
292 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  ( ( deg1  ` fld ) `
 a )  e. 
NN0 )
293291, 292eqeltrd 2511 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  NN0  ->  if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
294 mnflt0 11097 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |- -oo  <  0
295 mnfxr 11086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |- -oo  e.  RR*
296 xrltnle 9435 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( -oo  e.  RR*  /\  0  e.  RR* )  ->  ( -oo  <  0  <->  -.  0  <_ -oo ) )
297295, 270, 296mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( -oo  <  0  <->  -.  0  <_ -oo )
298294, 297mpbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -.  0  <_ -oo
299 elsni 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  ( ( deg1  ` fld ) `  a )  = -oo )
300299breq2d 4297 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  ( 0  <_  (
( deg1  `
fld ) `  a )  <->  0  <_ -oo )
)
301298, 300mtbiri 303 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  -.  0  <_  (
( deg1  `
fld ) `  a ) )
302 iffalse 3792 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  0  <_  ( ( deg1  ` fld ) `  a )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  0 )
303301, 302syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  =  0 )
304 0nn0 10586 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  NN0
305303, 304syl6eqel 2525 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( deg1  ` fld ) `  a )  e.  { -oo }  ->  if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
306293, 305jaoi 379 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( deg1  ` fld ) `  a )  e.  NN0  \/  (
( deg1  `
fld ) `  a )  e.  { -oo }
)  ->  if (
0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
307288, 306syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
308307ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 )  e. 
NN0 )
309 fznn0 11516 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
310308, 309syl 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 ) ) ) )
311284, 310sylibrd 234 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
( (coe1 `  a ) `  k )  =/=  0  ->  k  e.  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )
312311necon1bd 2673 . . . . . . . . . . . . . . . . 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 ) )
313262, 312mpd 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 )
314313oveq1d 6101 . . . . . . . . . . . . . . 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 ) ) )
315264, 253sylan2 474 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  /\  z  e.  CC )  /\  k  e.  ( NN0  \  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
z ^ k )  e.  CC )
316315mul02d 9559 . . . . . . . . . . . . . . 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 )
317314, 316eqtrd 2469 . . . . . . . . . . . . . 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 )
318317an32s 802 . . . . . . . . . . . . 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 )
319318mpteq2dva 4371 . . . . . . . . . . . 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 ) )
320 fconstmpt 4874 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( z  e.  CC  |->  0 )
321 rngmnd 16640 . . . . . . . . . . . . . . 15  |-  (fld  e.  Ring  ->fld  e.  Mnd )
3229, 321ax-mp 5 . . . . . . . . . . . . . 14  |-fld  e.  Mnd
3233, 17pws0g 15449 . . . . . . . . . . . . . 14  |-  ( (fld  e. 
Mnd  /\  CC  e.  _V )  ->  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) ) )
324322, 6, 323mp2an 672 . . . . . . . . . . . . 13  |-  ( CC 
X.  { 0 } )  =  ( 0g
`  (fld 
^s 
CC ) )
325320, 324eqtr3i 2459 . . . . . . . . . . . 12  |-  ( z  e.  CC  |->  0 )  =  ( 0g `  (fld  ^s  CC ) )
326319, 325syl6eq 2485 . . . . . . . . . . 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 ) ) )
327326, 169suppss2 6718 . . . . . . . . . 10  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) ) supp  ( 0g `  (fld  ^s  CC ) ) )  C_  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )
328 suppssfifsupp 7627 . . . . . . . . . 10  |-  ( ( ( ( k  e. 
NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k
)  x.  ( z ^ k ) ) ) )  e.  _V  /\ 
Fun  ( k  e. 
NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k
)  x.  ( z ^ k ) ) ) )  /\  ( 0g `  (fld 
^s 
CC ) )  e. 
_V )  /\  (
( 0 ... if ( 0  <_  (
( deg1  `
fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  e.  Fin  /\  (
( k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a
) `  k )  x.  ( z ^ k
) ) ) ) supp  ( 0g `  (fld  ^s  CC ) ) )  C_  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) ) )  ->  (
k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) ) finSupp  ( 0g `  (fld 
^s 
CC ) ) )
329259, 260, 327, 328syl12anc 1216 . . . . . . . . 9  |-  ( ( S  e.  (SubRing ` fld )  /\  a  e.  A )  ->  (
k  e.  NN0  |->  ( z  e.  CC  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) ) ) finSupp  ( 0g `  (fld 
^s 
CC ) ) )
3303, 4, 5, 250, 169, 251, 255, 329pwsgsum 16459 . . . . . . . 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
) ) ) ) ) )
331 elfznn0 11473 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) )  ->  k  e.  NN0 )
332331ssriv 3353 . . . . . . . . . . . 12  |-  ( 0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) 
C_  NN0
333 resmpt 5149 . . . . . . . . . . . 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
) ) ) )
334332, 333ax-mp 5 . . . . . . . . . . 11  |-  ( ( k  e.  NN0  |->  ( ( (coe1 `  a ) `  k )  x.  (
z ^ k ) ) )  |`  (
0 ... if ( 0  <_  ( ( deg1  ` fld ) `  a ) ,  ( ( deg1  ` fld ) `  a ) ,  0 ) ) )  =  ( k  e.  ( 0 ...
if ( 0  <_ 
( ( deg1  ` fld ) `  a ) ,  (