Metamath Proof Explorer

Theorem plymullem

Description: Lemma for plymul . (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 ) ) ) )
plymul.x 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
Assertion plymullem 
|- ( ph -> ( F oF x. 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 plymul.x 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
13 plybss 
 |-  ( F e. ( Poly ` S ) -> S C_ CC )
14 1 13 syl 
 |-  ( ph -> S C_ CC )
15 0cnd 
 |-  ( ph -> 0 e. CC )
16 15 snssd 
 |-  ( ph -> { 0 } C_ CC )
17 14 16 unssd 
 |-  ( ph -> ( S u. { 0 } ) C_ CC )
18 cnex 
 |-  CC e. _V
19 ssexg 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ CC e. _V ) -> ( S u. { 0 } ) e. _V )
20 17 18 19 sylancl 
 |-  ( ph -> ( S u. { 0 } ) e. _V )
21 nn0ex 
 |-  NN0 e. _V
22 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
23 20 21 22 sylancl 
 |-  ( ph -> ( A e. ( ( S u. { 0 } ) ^m NN0 ) <-> A : NN0 --> ( S u. { 0 } ) ) )
24 6 23 mpbid 
 |-  ( ph -> A : NN0 --> ( S u. { 0 } ) )
25 24 17 fssd 
 |-  ( ph -> A : NN0 --> CC )
26 elmapg 
 |-  ( ( ( S u. { 0 } ) e. _V /\ NN0 e. _V ) -> ( B e. ( ( S u. { 0 } ) ^m NN0 ) <-> B : NN0 --> ( S u. { 0 } ) ) )
27 20 21 26 sylancl 
 |-  ( ph -> ( B e. ( ( S u. { 0 } ) ^m NN0 ) <-> B : NN0 --> ( S u. { 0 } ) ) )
28 7 27 mpbid 
 |-  ( ph -> B : NN0 --> ( S u. { 0 } ) )
29 28 17 fssd 
 |-  ( ph -> B : NN0 --> CC )
30 1 2 4 5 25 29 8 9 10 11 plymullem1 
 |-  ( ph -> ( F oF x. G ) = ( z e. CC |-> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) ) )
31 4 5 nn0addcld 
 |-  ( ph -> ( M + N ) e. NN0 )
32 eqid 
 |-  ( S u. { 0 } ) = ( S u. { 0 } )
33 14 32 3 un0addcl 
 |-  ( ( ph /\ ( x e. ( S u. { 0 } ) /\ y e. ( S u. { 0 } ) ) ) -> ( x + y ) e. ( S u. { 0 } ) )
34 fzfid 
 |-  ( ph -> ( 0 ... n ) e. Fin )
35 elfznn0 
 |-  ( k e. ( 0 ... n ) -> k e. NN0 )
36 ffvelrn 
 |-  ( ( A : NN0 --> ( S u. { 0 } ) /\ k e. NN0 ) -> ( A ` k ) e. ( S u. { 0 } ) )
37 24 35 36 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... n ) ) -> ( A ` k ) e. ( S u. { 0 } ) )
38 fznn0sub 
 |-  ( k e. ( 0 ... n ) -> ( n - k ) e. NN0 )
39 ffvelrn 
 |-  ( ( B : NN0 --> ( S u. { 0 } ) /\ ( n - k ) e. NN0 ) -> ( B ` ( n - k ) ) e. ( S u. { 0 } ) )
40 28 38 39 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... n ) ) -> ( B ` ( n - k ) ) e. ( S u. { 0 } ) )
41 37 40 jca 
 |-  ( ( ph /\ k e. ( 0 ... n ) ) -> ( ( A ` k ) e. ( S u. { 0 } ) /\ ( B ` ( n - k ) ) e. ( S u. { 0 } ) ) )
42 14 32 12 un0mulcl 
 |-  ( ( ph /\ ( x e. ( S u. { 0 } ) /\ y e. ( S u. { 0 } ) ) ) -> ( x x. y ) e. ( S u. { 0 } ) )
43 42 caovclg 
 |-  ( ( ph /\ ( ( A ` k ) e. ( S u. { 0 } ) /\ ( B ` ( n - k ) ) e. ( S u. { 0 } ) ) ) -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) e. ( S u. { 0 } ) )
44 41 43 syldan 
 |-  ( ( ph /\ k e. ( 0 ... n ) ) -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) e. ( S u. { 0 } ) )
45 ssun2 
 |-  { 0 } C_ ( S u. { 0 } )
46 c0ex 
 |-  0 e. _V
47 46 snss 
 |-  ( 0 e. ( S u. { 0 } ) <-> { 0 } C_ ( S u. { 0 } ) )
48 45 47 mpbir 
 |-  0 e. ( S u. { 0 } )
49 48 a1i 
 |-  ( ph -> 0 e. ( S u. { 0 } ) )
50 17 33 34 44 49 fsumcllem 
 |-  ( ph -> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) e. ( S u. { 0 } ) )
51 50 adantr 
 |-  ( ( ph /\ n e. ( 0 ... ( M + N ) ) ) -> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) e. ( S u. { 0 } ) )
52 17 31 51 elplyd 
 |-  ( ph -> ( z e. CC |-> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) ) e. ( Poly ` ( S u. { 0 } ) ) )
53 30 52 eqeltrd 
 |-  ( ph -> ( F oF x. G ) e. ( Poly ` ( S u. { 0 } ) ) )
54 plyun0 
 |-  ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )
55 53 54 eleqtrdi 
 |-  ( ph -> ( F oF x. G ) e. ( Poly ` S ) )