Metamath Proof Explorer

Theorem plyaddlem

Description: Lemma for plyadd . (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 )
plyadd.m 
|- ( ph -> M e. NN0 )
plyadd.n 
|- ( ph -> N e. NN0 )
plyadd.a 
|- ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
plyadd.b 
|- ( ph -> B e. ( ( S u. { 0 } ) ^m NN0 ) )
plyadd.a2 
|- ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
plyadd.b2 
|- ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
plyadd.f 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
plyadd.g 
|- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
Assertion plyaddlem 
|- ( 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 plyadd.m 
 |-  ( ph -> M e. NN0 )
5 plyadd.n 
 |-  ( ph -> N e. NN0 )
6 plyadd.a 
 |-  ( ph -> A e. ( ( S u. { 0 } ) ^m NN0 ) )
7 plyadd.b 
 |-  ( ph -> B e. ( ( S u. { 0 } ) ^m NN0 ) )
8 plyadd.a2 
 |-  ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
9 plyadd.b2 
 |-  ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
10 plyadd.f 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
11 plyadd.g 
 |-  ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
12 plybss 
 |-  ( F e. ( Poly ` S ) -> S C_ CC )
13 1 12 syl 
 |-  ( ph -> S C_ CC )
14 0cnd 
 |-  ( ph -> 0 e. CC )
15 14 snssd 
 |-  ( ph -> { 0 } C_ CC )
16 13 15 unssd 
 |-  ( ph -> ( S u. { 0 } ) C_ CC )
17 cnex 
 |-  CC e. _V
18 ssexg 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
19 16 17 18 sylancl 
 |-  ( ph -> ( S u. { 0 } ) e. _V )
20 nn0ex 
 |-  NN0 e. _V
21 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
22 19 20 21 sylancl 
 |-  ( ph -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
23 6 22 mpbid 
 |-  ( ph -> A : NN0 --> ( S u. { 0 } ) )
24 23 16 fssd 
 |-  ( ph -> A : NN0 --> CC )
25 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( B e. ( ( S u. { 0 } ) ^m NN0 ) <-> B : NN0 --> ( S u. { 0 } ) ) )
26 19 20 25 sylancl 
 |-  ( ph -> ( B e. ( ( S u. { 0 } ) ^m NN0 ) <-> B : NN0 --> ( S u. { 0 } ) ) )
27 7 26 mpbid 
 |-  ( ph -> B : NN0 --> ( S u. { 0 } ) )
28 27 16 fssd 
 |-  ( ph -> B : NN0 --> CC )
29 1 2 4 5 24 28 8 9 10 11 plyaddlem1 
 |-  ( ph -> ( F oF + G ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) ) )
30 5 4 ifcld 
 |-  ( ph -> if ( M <_ N , N , M ) e. NN0 )
31 eqid 
 |-  ( S u. { 0 } ) = ( S u. { 0 } )
32 13 31 3 un0addcl 
 |-  ( ( ph /\ ( x e. ( S u. { 0 } ) /\ y e. ( S u. { 0 } ) ) ) -> ( x + y ) e. ( S u. { 0 } ) )
33 20 a1i 
 |-  ( ph -> NN0 e. _V )
34 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
35 32 23 27 33 33 34 off 
 |-  ( ph -> ( A oF + B ) : NN0 --> ( S u. { 0 } ) )
36 elfznn0 
 |-  ( k e. ( 0 ... if ( M <_ N , N , M ) ) -> k e. NN0 )
37 ffvelcdm 
 |-  ( ( ( A oF + B ) : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( ( A oF + B ) ` k ) e. ( S u. { 0 } ) )
38 35 36 37 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... if ( M <_ N , N , M ) ) ) -> ( ( A oF + B ) ` k ) e. ( S u. { 0 } ) )
39 16 30 38 elplyd 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) ) e. ( Poly ` ( S u. { 0 } ) ) )
40 29 39 eqeltrd 
 |-  ( ph -> ( F oF + G ) e. ( Poly ` ( S u. { 0 } ) ) )
41 plyun0 
 |-  ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )
42 40 41 eleqtrdi 
 |-  ( ph -> ( F oF + G ) e. ( Poly ` S ) )