Metamath Proof Explorer


Theorem plyadd

Description: The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014)

Ref Expression
Hypotheses plyadd.1
|- ( ph -> F e. ( Poly ` S ) )
plyadd.2
|- ( ph -> G e. ( Poly ` S ) )
plyadd.3
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
Assertion plyadd
|- ( ph -> ( F oF + G ) e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 plyadd.1
 |-  ( ph -> F e. ( Poly ` S ) )
2 plyadd.2
 |-  ( ph -> G e. ( Poly ` S ) )
3 plyadd.3
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
4 elply2
 |-  ( F e. ( Poly ` S ) <-> ( S C_ CC /\ E. m e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) ) )
5 4 simprbi
 |-  ( F e. ( Poly ` S ) -> E. m e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
6 1 5 syl
 |-  ( ph -> E. m e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
7 elply2
 |-  ( G e. ( Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) )
8 7 simprbi
 |-  ( G e. ( Poly ` S ) -> E. n e. NN0 E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) )
9 2 8 syl
 |-  ( ph -> E. n e. NN0 E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) )
10 reeanv
 |-  ( E. m e. NN0 E. n e. NN0 ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) <-> ( E. m e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. n e. NN0 E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) )
11 reeanv
 |-  ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) <-> ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) )
12 simp1l
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> ph )
13 12 1 syl
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> F e. ( Poly ` S ) )
14 12 2 syl
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> G e. ( Poly ` S ) )
15 12 3 sylan
 |-  ( ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
16 simp1rl
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> m e. NN0 )
17 simp1rr
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> n e. NN0 )
18 simp2l
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> a e. ( ( S u. { 0 } ) ^m NN0 ) )
19 simp2r
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> b e. ( ( S u. { 0 } ) ^m NN0 ) )
20 simp3ll
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } )
21 simp3rl
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } )
22 simp3lr
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) )
23 oveq1
 |-  ( z = w -> ( z ^ k ) = ( w ^ k ) )
24 23 oveq2d
 |-  ( z = w -> ( ( a ` k ) x. ( z ^ k ) ) = ( ( a ` k ) x. ( w ^ k ) ) )
25 24 sumeq2sdv
 |-  ( z = w -> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( w ^ k ) ) )
26 fveq2
 |-  ( k = j -> ( a ` k ) = ( a ` j ) )
27 oveq2
 |-  ( k = j -> ( w ^ k ) = ( w ^ j ) )
28 26 27 oveq12d
 |-  ( k = j -> ( ( a ` k ) x. ( w ^ k ) ) = ( ( a ` j ) x. ( w ^ j ) ) )
29 28 cbvsumv
 |-  sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( w ^ k ) ) = sum_ j e. ( 0 ... m ) ( ( a ` j ) x. ( w ^ j ) )
30 25 29 eqtrdi
 |-  ( z = w -> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) = sum_ j e. ( 0 ... m ) ( ( a ` j ) x. ( w ^ j ) ) )
31 30 cbvmptv
 |-  ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) = ( w e. CC |-> sum_ j e. ( 0 ... m ) ( ( a ` j ) x. ( w ^ j ) ) )
32 22 31 eqtrdi
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> F = ( w e. CC |-> sum_ j e. ( 0 ... m ) ( ( a ` j ) x. ( w ^ j ) ) ) )
33 simp3rr
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) )
34 23 oveq2d
 |-  ( z = w -> ( ( b ` k ) x. ( z ^ k ) ) = ( ( b ` k ) x. ( w ^ k ) ) )
35 34 sumeq2sdv
 |-  ( z = w -> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( w ^ k ) ) )
36 fveq2
 |-  ( k = j -> ( b ` k ) = ( b ` j ) )
37 36 27 oveq12d
 |-  ( k = j -> ( ( b ` k ) x. ( w ^ k ) ) = ( ( b ` j ) x. ( w ^ j ) ) )
38 37 cbvsumv
 |-  sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( w ^ k ) ) = sum_ j e. ( 0 ... n ) ( ( b ` j ) x. ( w ^ j ) )
39 35 38 eqtrdi
 |-  ( z = w -> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) = sum_ j e. ( 0 ... n ) ( ( b ` j ) x. ( w ^ j ) ) )
40 39 cbvmptv
 |-  ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) = ( w e. CC |-> sum_ j e. ( 0 ... n ) ( ( b ` j ) x. ( w ^ j ) ) )
41 33 40 eqtrdi
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> G = ( w e. CC |-> sum_ j e. ( 0 ... n ) ( ( b ` j ) x. ( w ^ j ) ) ) )
42 13 14 15 16 17 18 19 20 21 32 41 plyaddlem
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) /\ ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) ) -> ( F oF + G ) e. ( Poly ` S ) )
43 42 3expia
 |-  ( ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) /\ ( a e. ( ( S u. { 0 } ) ^m NN0 ) /\ b e. ( ( S u. { 0 } ) ^m NN0 ) ) ) -> ( ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> ( F oF + G ) e. ( Poly ` S ) ) )
44 43 rexlimdvva
 |-  ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) -> ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> ( F oF + G ) e. ( Poly ` S ) ) )
45 11 44 syl5bir
 |-  ( ( ph /\ ( m e. NN0 /\ n e. NN0 ) ) -> ( ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> ( F oF + G ) e. ( Poly ` S ) ) )
46 45 rexlimdvva
 |-  ( ph -> ( E. m e. NN0 E. n e. NN0 ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> ( F oF + G ) e. ( Poly ` S ) ) )
47 10 46 syl5bir
 |-  ( ph -> ( ( E. m e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) ( ( a " ( ZZ>= ` ( m + 1 ) ) ) = { 0 } /\ F = ( z e. CC |-> sum_ k e. ( 0 ... m ) ( ( a ` k ) x. ( z ^ k ) ) ) ) /\ E. n e. NN0 E. b e. ( ( S u. { 0 } ) ^m NN0 ) ( ( b " ( ZZ>= ` ( n + 1 ) ) ) = { 0 } /\ G = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( b ` k ) x. ( z ^ k ) ) ) ) ) -> ( F oF + G ) e. ( Poly ` S ) ) )
48 6 9 47 mp2and
 |-  ( ph -> ( F oF + G ) e. ( Poly ` S ) )