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

Theorem plyco 23188
Description: The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
plyco.1  |-  ( ph  ->  F  e.  (Poly `  S ) )
plyco.2  |-  ( ph  ->  G  e.  (Poly `  S ) )
plyco.3  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  +  y )  e.  S )
plyco.4  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  x.  y
)  e.  S )
Assertion
Ref Expression
plyco  |-  ( ph  ->  ( F  o.  G
)  e.  (Poly `  S ) )
Distinct variable groups:    x, y, F    x, G, y    ph, x, y    x, S, y

Proof of Theorem plyco
Dummy variables  k 
d  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 plyco.2 . . . . 5  |-  ( ph  ->  G  e.  (Poly `  S ) )
2 plyf 23145 . . . . 5  |-  ( G  e.  (Poly `  S
)  ->  G : CC
--> CC )
31, 2syl 17 . . . 4  |-  ( ph  ->  G : CC --> CC )
43ffvelrnda 6020 . . 3  |-  ( (
ph  /\  z  e.  CC )  ->  ( G `
 z )  e.  CC )
53feqmptd 5916 . . 3  |-  ( ph  ->  G  =  ( z  e.  CC  |->  ( G `
 z ) ) )
6 plyco.1 . . . 4  |-  ( ph  ->  F  e.  (Poly `  S ) )
7 eqid 2450 . . . . 5  |-  (coeff `  F )  =  (coeff `  F )
8 eqid 2450 . . . . 5  |-  (deg `  F )  =  (deg
`  F )
97, 8coeid 23185 . . . 4  |-  ( F  e.  (Poly `  S
)  ->  F  =  ( x  e.  CC  |->  sum_ k  e.  ( 0 ... (deg `  F
) ) ( ( (coeff `  F ) `  k )  x.  (
x ^ k ) ) ) )
106, 9syl 17 . . 3  |-  ( ph  ->  F  =  ( x  e.  CC  |->  sum_ k  e.  ( 0 ... (deg `  F ) ) ( ( (coeff `  F
) `  k )  x.  ( x ^ k
) ) ) )
11 oveq1 6295 . . . . 5  |-  ( x  =  ( G `  z )  ->  (
x ^ k )  =  ( ( G `
 z ) ^
k ) )
1211oveq2d 6304 . . . 4  |-  ( x  =  ( G `  z )  ->  (
( (coeff `  F
) `  k )  x.  ( x ^ k
) )  =  ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )
1312sumeq2sdv 13763 . . 3  |-  ( x  =  ( G `  z )  ->  sum_ k  e.  ( 0 ... (deg `  F ) ) ( ( (coeff `  F
) `  k )  x.  ( x ^ k
) )  =  sum_ k  e.  ( 0 ... (deg `  F
) ) ( ( (coeff `  F ) `  k )  x.  (
( G `  z
) ^ k ) ) )
144, 5, 10, 13fmptco 6054 . 2  |-  ( ph  ->  ( F  o.  G
)  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... (deg `  F ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) ) )
15 dgrcl 23180 . . . 4  |-  ( F  e.  (Poly `  S
)  ->  (deg `  F
)  e.  NN0 )
166, 15syl 17 . . 3  |-  ( ph  ->  (deg `  F )  e.  NN0 )
17 oveq2 6296 . . . . . . . 8  |-  ( x  =  0  ->  (
0 ... x )  =  ( 0 ... 0
) )
1817sumeq1d 13760 . . . . . . 7  |-  ( x  =  0  ->  sum_ k  e.  ( 0 ... x
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  =  sum_ k  e.  ( 0 ... 0 ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )
1918mpteq2dv 4489 . . . . . 6  |-  ( x  =  0  ->  (
z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... 0 ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) ) )
2019eleq1d 2512 . . . . 5  |-  ( x  =  0  ->  (
( z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... 0 ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) )
2120imbi2d 318 . . . 4  |-  ( x  =  0  ->  (
( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... x
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) )  <->  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... 0 ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) ) )
22 oveq2 6296 . . . . . . . 8  |-  ( x  =  d  ->  (
0 ... x )  =  ( 0 ... d
) )
2322sumeq1d 13760 . . . . . . 7  |-  ( x  =  d  ->  sum_ k  e.  ( 0 ... x
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  =  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )
2423mpteq2dv 4489 . . . . . 6  |-  ( x  =  d  ->  (
z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) ) )
2524eleq1d 2512 . . . . 5  |-  ( x  =  d  ->  (
( z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) )
2625imbi2d 318 . . . 4  |-  ( x  =  d  ->  (
( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... x
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) )  <->  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) ) )
27 oveq2 6296 . . . . . . . 8  |-  ( x  =  ( d  +  1 )  ->  (
0 ... x )  =  ( 0 ... (
d  +  1 ) ) )
2827sumeq1d 13760 . . . . . . 7  |-  ( x  =  ( d  +  1 )  ->  sum_ k  e.  ( 0 ... x
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  =  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )
2928mpteq2dv 4489 . . . . . 6  |-  ( x  =  ( d  +  1 )  ->  (
z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) ) )
3029eleq1d 2512 . . . . 5  |-  ( x  =  ( d  +  1 )  ->  (
( z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) )
3130imbi2d 318 . . . 4  |-  ( x  =  ( d  +  1 )  ->  (
( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... x
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) )  <->  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) ) )
32 oveq2 6296 . . . . . . . 8  |-  ( x  =  (deg `  F
)  ->  ( 0 ... x )  =  ( 0 ... (deg `  F ) ) )
3332sumeq1d 13760 . . . . . . 7  |-  ( x  =  (deg `  F
)  ->  sum_ k  e.  ( 0 ... x
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  =  sum_ k  e.  ( 0 ... (deg `  F ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )
3433mpteq2dv 4489 . . . . . 6  |-  ( x  =  (deg `  F
)  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... (deg `  F ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) ) )
3534eleq1d 2512 . . . . 5  |-  ( x  =  (deg `  F
)  ->  ( (
z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... (deg `  F
) ) ( ( (coeff `  F ) `  k )  x.  (
( G `  z
) ^ k ) ) )  e.  (Poly `  S ) ) )
3635imbi2d 318 . . . 4  |-  ( x  =  (deg `  F
)  ->  ( ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... x ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) )  <->  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... (deg `  F
) ) ( ( (coeff `  F ) `  k )  x.  (
( G `  z
) ^ k ) ) )  e.  (Poly `  S ) ) ) )
37 0z 10945 . . . . . . . . 9  |-  0  e.  ZZ
384exp0d 12407 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  CC )  ->  ( ( G `  z ) ^ 0 )  =  1 )
3938oveq2d 6304 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  CC )  ->  ( ( (coeff `  F ) `  0 )  x.  ( ( G `  z ) ^ 0 ) )  =  ( ( (coeff `  F
) `  0 )  x.  1 ) )
40 plybss 23141 . . . . . . . . . . . . . . . 16  |-  ( F  e.  (Poly `  S
)  ->  S  C_  CC )
416, 40syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  S  C_  CC )
42 0cnd 9633 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  e.  CC )
4342snssd 4116 . . . . . . . . . . . . . . 15  |-  ( ph  ->  { 0 }  C_  CC )
4441, 43unssd 3609 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( S  u.  {
0 } )  C_  CC )
457coef 23177 . . . . . . . . . . . . . . . 16  |-  ( F  e.  (Poly `  S
)  ->  (coeff `  F
) : NN0 --> ( S  u.  { 0 } ) )
466, 45syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  (coeff `  F ) : NN0 --> ( S  u.  { 0 } ) )
47 0nn0 10881 . . . . . . . . . . . . . . 15  |-  0  e.  NN0
48 ffvelrn 6018 . . . . . . . . . . . . . . 15  |-  ( ( (coeff `  F ) : NN0 --> ( S  u.  { 0 } )  /\  0  e.  NN0 )  -> 
( (coeff `  F
) `  0 )  e.  ( S  u.  {
0 } ) )
4946, 47, 48sylancl 667 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( (coeff `  F
) `  0 )  e.  ( S  u.  {
0 } ) )
5044, 49sseldd 3432 . . . . . . . . . . . . 13  |-  ( ph  ->  ( (coeff `  F
) `  0 )  e.  CC )
5150adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  CC )  ->  ( (coeff `  F ) `  0
)  e.  CC )
5251mulid1d 9657 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  CC )  ->  ( ( (coeff `  F ) `  0 )  x.  1 )  =  ( (coeff `  F ) `  0 ) )
5339, 52eqtrd 2484 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  CC )  ->  ( ( (coeff `  F ) `  0 )  x.  ( ( G `  z ) ^ 0 ) )  =  ( (coeff `  F ) `  0 ) )
5453, 51eqeltrd 2528 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  CC )  ->  ( ( (coeff `  F ) `  0 )  x.  ( ( G `  z ) ^ 0 ) )  e.  CC )
55 fveq2 5863 . . . . . . . . . . 11  |-  ( k  =  0  ->  (
(coeff `  F ) `  k )  =  ( (coeff `  F ) `  0 ) )
56 oveq2 6296 . . . . . . . . . . 11  |-  ( k  =  0  ->  (
( G `  z
) ^ k )  =  ( ( G `
 z ) ^
0 ) )
5755, 56oveq12d 6306 . . . . . . . . . 10  |-  ( k  =  0  ->  (
( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) )  =  ( ( (coeff `  F
) `  0 )  x.  ( ( G `  z ) ^ 0 ) ) )
5857fsum1 13801 . . . . . . . . 9  |-  ( ( 0  e.  ZZ  /\  ( ( (coeff `  F ) `  0
)  x.  ( ( G `  z ) ^ 0 ) )  e.  CC )  ->  sum_ k  e.  ( 0 ... 0 ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) )  =  ( ( (coeff `  F
) `  0 )  x.  ( ( G `  z ) ^ 0 ) ) )
5937, 54, 58sylancr 668 . . . . . . . 8  |-  ( (
ph  /\  z  e.  CC )  ->  sum_ k  e.  ( 0 ... 0
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  =  ( ( (coeff `  F ) `  0
)  x.  ( ( G `  z ) ^ 0 ) ) )
6059, 53eqtrd 2484 . . . . . . 7  |-  ( (
ph  /\  z  e.  CC )  ->  sum_ k  e.  ( 0 ... 0
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  =  ( (coeff `  F ) `  0
) )
6160mpteq2dva 4488 . . . . . 6  |-  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... 0 ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  =  ( z  e.  CC  |->  ( (coeff `  F ) `  0 ) ) )
62 fconstmpt 4877 . . . . . 6  |-  ( CC 
X.  { ( (coeff `  F ) `  0
) } )  =  ( z  e.  CC  |->  ( (coeff `  F ) `  0 ) )
6361, 62syl6eqr 2502 . . . . 5  |-  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... 0 ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  =  ( CC  X.  {
( (coeff `  F
) `  0 ) } ) )
64 plyconst 23153 . . . . . . 7  |-  ( ( ( S  u.  {
0 } )  C_  CC  /\  ( (coeff `  F ) `  0
)  e.  ( S  u.  { 0 } ) )  ->  ( CC  X.  { ( (coeff `  F ) `  0
) } )  e.  (Poly `  ( S  u.  { 0 } ) ) )
6544, 49, 64syl2anc 666 . . . . . 6  |-  ( ph  ->  ( CC  X.  {
( (coeff `  F
) `  0 ) } )  e.  (Poly `  ( S  u.  {
0 } ) ) )
66 plyun0 23144 . . . . . 6  |-  (Poly `  ( S  u.  { 0 } ) )  =  (Poly `  S )
6765, 66syl6eleq 2538 . . . . 5  |-  ( ph  ->  ( CC  X.  {
( (coeff `  F
) `  0 ) } )  e.  (Poly `  S ) )
6863, 67eqeltrd 2528 . . . 4  |-  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... 0 ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
)
69 simprr 765 . . . . . . . . 9  |-  ( (
ph  /\  ( d  e.  NN0  /\  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) ) )  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) )
7044adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( S  u.  { 0 } ) 
C_  CC )
71 peano2nn0 10907 . . . . . . . . . . . . . 14  |-  ( d  e.  NN0  ->  ( d  +  1 )  e. 
NN0 )
72 ffvelrn 6018 . . . . . . . . . . . . . 14  |-  ( ( (coeff `  F ) : NN0 --> ( S  u.  { 0 } )  /\  ( d  +  1 )  e.  NN0 )  ->  ( (coeff `  F
) `  ( d  +  1 ) )  e.  ( S  u.  { 0 } ) )
7346, 71, 72syl2an 480 . . . . . . . . . . . . 13  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( (coeff `  F ) `  (
d  +  1 ) )  e.  ( S  u.  { 0 } ) )
74 plyconst 23153 . . . . . . . . . . . . 13  |-  ( ( ( S  u.  {
0 } )  C_  CC  /\  ( (coeff `  F ) `  (
d  +  1 ) )  e.  ( S  u.  { 0 } ) )  ->  ( CC  X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  e.  (Poly `  ( S  u.  { 0 } ) ) )
7570, 73, 74syl2anc 666 . . . . . . . . . . . 12  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( CC  X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  e.  (Poly `  ( S  u.  { 0 } ) ) )
7675, 66syl6eleq 2538 . . . . . . . . . . 11  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( CC  X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  e.  (Poly `  S )
)
77 nn0p1nn 10906 . . . . . . . . . . . . 13  |-  ( d  e.  NN0  ->  ( d  +  1 )  e.  NN )
78 oveq2 6296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  1  ->  (
( G `  z
) ^ x )  =  ( ( G `
 z ) ^
1 ) )
7978mpteq2dv 4489 . . . . . . . . . . . . . . . 16  |-  ( x  =  1  ->  (
z  e.  CC  |->  ( ( G `  z
) ^ x ) )  =  ( z  e.  CC  |->  ( ( G `  z ) ^ 1 ) ) )
8079eleq1d 2512 . . . . . . . . . . . . . . 15  |-  ( x  =  1  ->  (
( z  e.  CC  |->  ( ( G `  z ) ^ x
) )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  ( ( G `
 z ) ^
1 ) )  e.  (Poly `  S )
) )
8180imbi2d 318 . . . . . . . . . . . . . 14  |-  ( x  =  1  ->  (
( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ x ) )  e.  (Poly `  S
) )  <->  ( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ 1 ) )  e.  (Poly `  S ) ) ) )
82 oveq2 6296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  d  ->  (
( G `  z
) ^ x )  =  ( ( G `
 z ) ^
d ) )
8382mpteq2dv 4489 . . . . . . . . . . . . . . . 16  |-  ( x  =  d  ->  (
z  e.  CC  |->  ( ( G `  z
) ^ x ) )  =  ( z  e.  CC  |->  ( ( G `  z ) ^ d ) ) )
8483eleq1d 2512 . . . . . . . . . . . . . . 15  |-  ( x  =  d  ->  (
( z  e.  CC  |->  ( ( G `  z ) ^ x
) )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  ( ( G `
 z ) ^
d ) )  e.  (Poly `  S )
) )
8584imbi2d 318 . . . . . . . . . . . . . 14  |-  ( x  =  d  ->  (
( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ x ) )  e.  (Poly `  S
) )  <->  ( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ d
) )  e.  (Poly `  S ) ) ) )
86 oveq2 6296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( d  +  1 )  ->  (
( G `  z
) ^ x )  =  ( ( G `
 z ) ^
( d  +  1 ) ) )
8786mpteq2dv 4489 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( d  +  1 )  ->  (
z  e.  CC  |->  ( ( G `  z
) ^ x ) )  =  ( z  e.  CC  |->  ( ( G `  z ) ^ ( d  +  1 ) ) ) )
8887eleq1d 2512 . . . . . . . . . . . . . . 15  |-  ( x  =  ( d  +  1 )  ->  (
( z  e.  CC  |->  ( ( G `  z ) ^ x
) )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  ( ( G `
 z ) ^
( d  +  1 ) ) )  e.  (Poly `  S )
) )
8988imbi2d 318 . . . . . . . . . . . . . 14  |-  ( x  =  ( d  +  1 )  ->  (
( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ x ) )  e.  (Poly `  S
) )  <->  ( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ (
d  +  1 ) ) )  e.  (Poly `  S ) ) ) )
904exp1d 12408 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  z  e.  CC )  ->  ( ( G `  z ) ^ 1 )  =  ( G `  z
) )
9190mpteq2dva 4488 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ 1 ) )  =  ( z  e.  CC  |->  ( G `  z ) ) )
9291, 5eqtr4d 2487 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ 1 ) )  =  G )
9392, 1eqeltrd 2528 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ 1 ) )  e.  (Poly `  S ) )
94 simprr 765 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( d  e.  NN  /\  ( z  e.  CC  |->  ( ( G `  z ) ^ d ) )  e.  (Poly `  S
) ) )  -> 
( z  e.  CC  |->  ( ( G `  z ) ^ d
) )  e.  (Poly `  S ) )
951adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( d  e.  NN  /\  ( z  e.  CC  |->  ( ( G `  z ) ^ d ) )  e.  (Poly `  S
) ) )  ->  G  e.  (Poly `  S
) )
96 plyco.3 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  +  y )  e.  S )
9796adantlr 720 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
d  e.  NN  /\  ( z  e.  CC  |->  ( ( G `  z ) ^ d
) )  e.  (Poly `  S ) ) )  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  +  y )  e.  S )
98 plyco.4 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  x.  y
)  e.  S )
9998adantlr 720 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
d  e.  NN  /\  ( z  e.  CC  |->  ( ( G `  z ) ^ d
) )  e.  (Poly `  S ) ) )  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  x.  y
)  e.  S )
10094, 95, 97, 99plymul 23165 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( d  e.  NN  /\  ( z  e.  CC  |->  ( ( G `  z ) ^ d ) )  e.  (Poly `  S
) ) )  -> 
( ( z  e.  CC  |->  ( ( G `
 z ) ^
d ) )  oF  x.  G )  e.  (Poly `  S
) )
101100expr 619 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  NN )  ->  ( ( z  e.  CC  |->  ( ( G `  z
) ^ d ) )  e.  (Poly `  S )  ->  (
( z  e.  CC  |->  ( ( G `  z ) ^ d
) )  oF  x.  G )  e.  (Poly `  S )
) )
102 cnex 9617 . . . . . . . . . . . . . . . . . . . . 21  |-  CC  e.  _V
103102a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  NN )  ->  CC  e.  _V )
104 ovex 6316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G `  z ) ^ d )  e. 
_V
105104a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  NN )  /\  z  e.  CC )  ->  (
( G `  z
) ^ d )  e.  _V )
1064adantlr 720 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  NN )  /\  z  e.  CC )  ->  ( G `  z )  e.  CC )
107 eqidd 2451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  NN )  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ d ) )  =  ( z  e.  CC  |->  ( ( G `
 z ) ^
d ) ) )
1085adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  d  e.  NN )  ->  G  =  ( z  e.  CC  |->  ( G `  z ) ) )
109103, 105, 106, 107, 108offval2 6545 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  NN )  ->  ( ( z  e.  CC  |->  ( ( G `  z
) ^ d ) )  oF  x.  G )  =  ( z  e.  CC  |->  ( ( ( G `  z ) ^ d
)  x.  ( G `
 z ) ) ) )
110 nnnn0 10873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  e.  NN  ->  d  e.  NN0 )
111110ad2antlr 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  d  e.  NN )  /\  z  e.  CC )  ->  d  e.  NN0 )
112106, 111expp1d 12414 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  d  e.  NN )  /\  z  e.  CC )  ->  (
( G `  z
) ^ ( d  +  1 ) )  =  ( ( ( G `  z ) ^ d )  x.  ( G `  z
) ) )
113112mpteq2dva 4488 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  d  e.  NN )  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ ( d  +  1 ) ) )  =  ( z  e.  CC  |->  ( ( ( G `  z ) ^ d )  x.  ( G `  z
) ) ) )
114109, 113eqtr4d 2487 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  d  e.  NN )  ->  ( ( z  e.  CC  |->  ( ( G `  z
) ^ d ) )  oF  x.  G )  =  ( z  e.  CC  |->  ( ( G `  z
) ^ ( d  +  1 ) ) ) )
115114eleq1d 2512 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  d  e.  NN )  ->  ( ( ( z  e.  CC  |->  ( ( G `  z ) ^ d
) )  oF  x.  G )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  ( ( G `  z
) ^ ( d  +  1 ) ) )  e.  (Poly `  S ) ) )
116101, 115sylibd 218 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  d  e.  NN )  ->  ( ( z  e.  CC  |->  ( ( G `  z
) ^ d ) )  e.  (Poly `  S )  ->  (
z  e.  CC  |->  ( ( G `  z
) ^ ( d  +  1 ) ) )  e.  (Poly `  S ) ) )
117116expcom 437 . . . . . . . . . . . . . . 15  |-  ( d  e.  NN  ->  ( ph  ->  ( ( z  e.  CC  |->  ( ( G `  z ) ^ d ) )  e.  (Poly `  S
)  ->  ( z  e.  CC  |->  ( ( G `
 z ) ^
( d  +  1 ) ) )  e.  (Poly `  S )
) ) )
118117a2d 29 . . . . . . . . . . . . . 14  |-  ( d  e.  NN  ->  (
( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ d ) )  e.  (Poly `  S
) )  ->  ( ph  ->  ( z  e.  CC  |->  ( ( G `
 z ) ^
( d  +  1 ) ) )  e.  (Poly `  S )
) ) )
11981, 85, 89, 89, 93, 118nnind 10624 . . . . . . . . . . . . 13  |-  ( ( d  +  1 )  e.  NN  ->  ( ph  ->  ( z  e.  CC  |->  ( ( G `
 z ) ^
( d  +  1 ) ) )  e.  (Poly `  S )
) )
12077, 119syl 17 . . . . . . . . . . . 12  |-  ( d  e.  NN0  ->  ( ph  ->  ( z  e.  CC  |->  ( ( G `  z ) ^ (
d  +  1 ) ) )  e.  (Poly `  S ) ) )
121120impcom 432 . . . . . . . . . . 11  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( z  e.  CC  |->  ( ( G `
 z ) ^
( d  +  1 ) ) )  e.  (Poly `  S )
)
12296adantlr 720 . . . . . . . . . . 11  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  +  y )  e.  S )
12398adantlr 720 . . . . . . . . . . 11  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  x.  y )  e.  S
)
12476, 121, 122, 123plymul 23165 . . . . . . . . . 10  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( ( CC  X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  oF  x.  ( z  e.  CC  |->  ( ( G `  z ) ^ ( d  +  1 ) ) ) )  e.  (Poly `  S ) )
125124adantrr 722 . . . . . . . . 9  |-  ( (
ph  /\  ( d  e.  NN0  /\  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) ) )  ->  ( ( CC 
X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  oF  x.  ( z  e.  CC  |->  ( ( G `  z ) ^ ( d  +  1 ) ) ) )  e.  (Poly `  S ) )
12696adantlr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  (
d  e.  NN0  /\  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) )  /\  (
x  e.  S  /\  y  e.  S )
)  ->  ( x  +  y )  e.  S )
12769, 125, 126plyadd 23164 . . . . . . . 8  |-  ( (
ph  /\  ( d  e.  NN0  /\  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) ) )  ->  ( ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  oF  +  ( ( CC  X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  oF  x.  ( z  e.  CC  |->  ( ( G `  z ) ^ ( d  +  1 ) ) ) ) )  e.  (Poly `  S ) )
128127expr 619 . . . . . . 7  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( (
z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )  ->  ( ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  oF  +  ( ( CC  X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  oF  x.  ( z  e.  CC  |->  ( ( G `  z ) ^ ( d  +  1 ) ) ) ) )  e.  (Poly `  S ) ) )
129102a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  d  e.  NN0 )  ->  CC  e.  _V )
130 sumex 13747 . . . . . . . . . . 11  |-  sum_ k  e.  ( 0 ... d
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  e.  _V
131130a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  sum_ k  e.  ( 0 ... d
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  e.  _V )
132 ovex 6316 . . . . . . . . . . 11  |-  ( ( (coeff `  F ) `  ( d  +  1 ) )  x.  (
( G `  z
) ^ ( d  +  1 ) ) )  e.  _V
133132a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  (
( (coeff `  F
) `  ( d  +  1 ) )  x.  ( ( G `
 z ) ^
( d  +  1 ) ) )  e. 
_V )
134 eqidd 2451 . . . . . . . . . 10  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) ) )
135 fvex 5873 . . . . . . . . . . . 12  |-  ( (coeff `  F ) `  (
d  +  1 ) )  e.  _V
136135a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  (
(coeff `  F ) `  ( d  +  1 ) )  e.  _V )
137 ovex 6316 . . . . . . . . . . . 12  |-  ( ( G `  z ) ^ ( d  +  1 ) )  e. 
_V
138137a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  (
( G `  z
) ^ ( d  +  1 ) )  e.  _V )
139 fconstmpt 4877 . . . . . . . . . . . 12  |-  ( CC 
X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  =  ( z  e.  CC  |->  ( (coeff `  F ) `  ( d  +  1 ) ) )
140139a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( CC  X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  =  ( z  e.  CC  |->  ( (coeff `  F ) `  ( d  +  1 ) ) ) )
141 eqidd 2451 . . . . . . . . . . 11  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( z  e.  CC  |->  ( ( G `
 z ) ^
( d  +  1 ) ) )  =  ( z  e.  CC  |->  ( ( G `  z ) ^ (
d  +  1 ) ) ) )
142129, 136, 138, 140, 141offval2 6545 . . . . . . . . . 10  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( ( CC  X.  { ( (coeff `  F ) `  (
d  +  1 ) ) } )  oF  x.  ( z  e.  CC  |->  ( ( G `  z ) ^ ( d  +  1 ) ) ) )  =  ( z  e.  CC  |->  ( ( (coeff `  F ) `  ( d  +  1 ) )  x.  (
( G `  z
) ^ ( d  +  1 ) ) ) ) )
143129, 131, 133, 134, 142offval2 6545 . . . . . . . . 9  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( (
z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  oF  +  ( ( CC  X.  { ( (coeff `  F ) `  ( d  +  1 ) ) } )  oF  x.  (
z  e.  CC  |->  ( ( G `  z
) ^ ( d  +  1 ) ) ) ) )  =  ( z  e.  CC  |->  ( sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  +  ( ( (coeff `  F ) `  (
d  +  1 ) )  x.  ( ( G `  z ) ^ ( d  +  1 ) ) ) ) ) )
144 simplr 761 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  d  e.  NN0 )
145 nn0uz 11190 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
146144, 145syl6eleq 2538 . . . . . . . . . . 11  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  d  e.  ( ZZ>= `  0 )
)
1477coef3 23179 . . . . . . . . . . . . . . 15  |-  ( F  e.  (Poly `  S
)  ->  (coeff `  F
) : NN0 --> CC )
1486, 147syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  (coeff `  F ) : NN0 --> CC )
149148ad2antrr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  (coeff `  F ) : NN0 --> CC )
150 elfznn0 11884 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... ( d  +  1 ) )  ->  k  e.  NN0 )
151 ffvelrn 6018 . . . . . . . . . . . . 13  |-  ( ( (coeff `  F ) : NN0 --> CC  /\  k  e.  NN0 )  ->  (
(coeff `  F ) `  k )  e.  CC )
152149, 150, 151syl2an 480 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  /\  k  e.  (
0 ... ( d  +  1 ) ) )  ->  ( (coeff `  F ) `  k
)  e.  CC )
1534adantlr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  ( G `  z )  e.  CC )
154 expcl 12287 . . . . . . . . . . . . 13  |-  ( ( ( G `  z
)  e.  CC  /\  k  e.  NN0 )  -> 
( ( G `  z ) ^ k
)  e.  CC )
155153, 150, 154syl2an 480 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  /\  k  e.  (
0 ... ( d  +  1 ) ) )  ->  ( ( G `
 z ) ^
k )  e.  CC )
156152, 155mulcld 9660 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  /\  k  e.  (
0 ... ( d  +  1 ) ) )  ->  ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  e.  CC )
157 fveq2 5863 . . . . . . . . . . . 12  |-  ( k  =  ( d  +  1 )  ->  (
(coeff `  F ) `  k )  =  ( (coeff `  F ) `  ( d  +  1 ) ) )
158 oveq2 6296 . . . . . . . . . . . 12  |-  ( k  =  ( d  +  1 )  ->  (
( G `  z
) ^ k )  =  ( ( G `
 z ) ^
( d  +  1 ) ) )
159157, 158oveq12d 6306 . . . . . . . . . . 11  |-  ( k  =  ( d  +  1 )  ->  (
( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) )  =  ( ( (coeff `  F
) `  ( d  +  1 ) )  x.  ( ( G `
 z ) ^
( d  +  1 ) ) ) )
160146, 156, 159fsump1 13810 . . . . . . . . . 10  |-  ( ( ( ph  /\  d  e.  NN0 )  /\  z  e.  CC )  ->  sum_ k  e.  ( 0 ... (
d  +  1 ) ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  =  ( sum_ k  e.  ( 0 ... d
) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) )  +  ( ( (coeff `  F ) `  (
d  +  1 ) )  x.  ( ( G `  z ) ^ ( d  +  1 ) ) ) ) )
161160mpteq2dva 4488 . . . . . . . . 9  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  =  ( z  e.  CC  |->  ( sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) )  +  ( ( (coeff `  F
) `  ( d  +  1 ) )  x.  ( ( G `
 z ) ^
( d  +  1 ) ) ) ) ) )
162143, 161eqtr4d 2487 . . . . . . . 8  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( (
z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  oF  +  ( ( CC  X.  { ( (coeff `  F ) `  ( d  +  1 ) ) } )  oF  x.  (
z  e.  CC  |->  ( ( G `  z
) ^ ( d  +  1 ) ) ) ) )  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) ) )
163162eleq1d 2512 . . . . . . 7  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( (
( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  oF  +  ( ( CC  X.  { ( (coeff `  F ) `  ( d  +  1 ) ) } )  oF  x.  (
z  e.  CC  |->  ( ( G `  z
) ^ ( d  +  1 ) ) ) ) )  e.  (Poly `  S )  <->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) )
164128, 163sylibd 218 . . . . . 6  |-  ( (
ph  /\  d  e.  NN0 )  ->  ( (
z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) )
165164expcom 437 . . . . 5  |-  ( d  e.  NN0  ->  ( ph  ->  ( ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S )  ->  (
z  e.  CC  |->  sum_ k  e.  ( 0 ... ( d  +  1 ) ) ( ( (coeff `  F
) `  k )  x.  ( ( G `  z ) ^ k
) ) )  e.  (Poly `  S )
) ) )
166165a2d 29 . . . 4  |-  ( d  e.  NN0  ->  ( (
ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... d ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) )  -> 
( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... (
d  +  1 ) ) ( ( (coeff `  F ) `  k
)  x.  ( ( G `  z ) ^ k ) ) )  e.  (Poly `  S ) ) ) )
16721, 26, 31, 36, 68, 166nn0ind 11027 . . 3  |-  ( (deg
`  F )  e. 
NN0  ->  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... (deg `  F
) ) ( ( (coeff `  F ) `  k )  x.  (
( G `  z
) ^ k ) ) )  e.  (Poly `  S ) ) )
16816, 167mpcom 37 . 2  |-  ( ph  ->  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... (deg `  F
) ) ( ( (coeff `  F ) `  k )  x.  (
( G `  z
) ^ k ) ) )  e.  (Poly `  S ) )
16914, 168eqeltrd 2528 1  |-  ( ph  ->  ( F  o.  G
)  e.  (Poly `  S ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1443    e. wcel 1886   _Vcvv 3044    u. cun 3401    C_ wss 3403   {csn 3967    |-> cmpt 4460    X. cxp 4831    o. ccom 4837   -->wf 5577   ` cfv 5581  (class class class)co 6288    oFcof 6526   CCcc 9534   0cc0 9536   1c1 9537    + caddc 9539    x. cmul 9541   NNcn 10606   NN0cn0 10866   ZZcz 10934   ZZ>=cuz 11156   ...cfz 11781   ^cexp 12269   sum_csu 13745  Polycply 23131  coeffccoe 23133  degcdgr 23134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-inf2 8143  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614  ax-addf 9615
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-fal 1449  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-of 6528  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-oadd 7183  df-er 7360  df-map 7471  df-pm 7472  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-sup 7953  df-inf 7954  df-oi 8022  df-card 8370  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-n0 10867  df-z 10935  df-uz 11157  df-rp 11300  df-fz 11782  df-fzo 11913  df-fl 12025  df-seq 12211  df-exp 12270  df-hash 12513  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-clim 13545  df-rlim 13546  df-sum 13746  df-0p 22621  df-ply 23135  df-coe 23137  df-dgr 23138
This theorem is referenced by:  dgrcolem1  23220  dgrcolem2  23221  taylply2  23316  ftalem7  23998
  Copyright terms: Public domain W3C validator