Metamath Proof Explorer


Theorem plymullem1

Description: Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypotheses plyaddlem.1
|- ( ph -> F e. ( Poly ` S ) )
plyaddlem.2
|- ( ph -> G e. ( Poly ` S ) )
plyaddlem.m
|- ( ph -> M e. NN0 )
plyaddlem.n
|- ( ph -> N e. NN0 )
plyaddlem.a
|- ( ph -> A : NN0 --> CC )
plyaddlem.b
|- ( ph -> B : NN0 --> CC )
plyaddlem.a2
|- ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
plyaddlem.b2
|- ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
plyaddlem.f
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
plyaddlem.g
|- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 plyaddlem.1
 |-  ( ph -> F e. ( Poly ` S ) )
2 plyaddlem.2
 |-  ( ph -> G e. ( Poly ` S ) )
3 plyaddlem.m
 |-  ( ph -> M e. NN0 )
4 plyaddlem.n
 |-  ( ph -> N e. NN0 )
5 plyaddlem.a
 |-  ( ph -> A : NN0 --> CC )
6 plyaddlem.b
 |-  ( ph -> B : NN0 --> CC )
7 plyaddlem.a2
 |-  ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
8 plyaddlem.b2
 |-  ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
9 plyaddlem.f
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
10 plyaddlem.g
 |-  ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
11 cnex
 |-  CC e. _V
12 11 a1i
 |-  ( ph -> CC e. _V )
13 sumex
 |-  sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) e. _V
14 13 a1i
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) e. _V )
15 sumex
 |-  sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) e. _V
16 15 a1i
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) e. _V )
17 12 14 16 9 10 offval2
 |-  ( ph -> ( F oF x. G ) = ( z e. CC |-> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ) )
18 fveq2
 |-  ( m = n -> ( B ` m ) = ( B ` n ) )
19 oveq2
 |-  ( m = n -> ( z ^ m ) = ( z ^ n ) )
20 18 19 oveq12d
 |-  ( m = n -> ( ( B ` m ) x. ( z ^ m ) ) = ( ( B ` n ) x. ( z ^ n ) ) )
21 20 oveq2d
 |-  ( m = n -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` m ) x. ( z ^ m ) ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
22 fveq2
 |-  ( m = ( n - k ) -> ( B ` m ) = ( B ` ( n - k ) ) )
23 oveq2
 |-  ( m = ( n - k ) -> ( z ^ m ) = ( z ^ ( n - k ) ) )
24 22 23 oveq12d
 |-  ( m = ( n - k ) -> ( ( B ` m ) x. ( z ^ m ) ) = ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) )
25 24 oveq2d
 |-  ( m = ( n - k ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` m ) x. ( z ^ m ) ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) )
26 elfznn0
 |-  ( k e. ( 0 ... ( M + N ) ) -> k e. NN0 )
27 5 adantr
 |-  ( ( ph /\ z e. CC ) -> A : NN0 --> CC )
28 27 ffvelrnda
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
29 expcl
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
30 29 adantll
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
31 28 30 mulcld
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
32 26 31 sylan2
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( M + N ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
33 elfznn0
 |-  ( n e. ( 0 ... ( ( M + N ) - k ) ) -> n e. NN0 )
34 6 adantr
 |-  ( ( ph /\ z e. CC ) -> B : NN0 --> CC )
35 34 ffvelrnda
 |-  ( ( ( ph /\ z e. CC ) /\ n e. NN0 ) -> ( B ` n ) e. CC )
36 expcl
 |-  ( ( z e. CC /\ n e. NN0 ) -> ( z ^ n ) e. CC )
37 36 adantll
 |-  ( ( ( ph /\ z e. CC ) /\ n e. NN0 ) -> ( z ^ n ) e. CC )
38 35 37 mulcld
 |-  ( ( ( ph /\ z e. CC ) /\ n e. NN0 ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
39 33 38 sylan2
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
40 32 39 anim12dan
 |-  ( ( ( ph /\ z e. CC ) /\ ( k e. ( 0 ... ( M + N ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) e. CC /\ ( ( B ` n ) x. ( z ^ n ) ) e. CC ) )
41 mulcl
 |-  ( ( ( ( A ` k ) x. ( z ^ k ) ) e. CC /\ ( ( B ` n ) x. ( z ^ n ) ) e. CC ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
42 40 41 syl
 |-  ( ( ( ph /\ z e. CC ) /\ ( k e. ( 0 ... ( M + N ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
43 21 25 42 fsum0diag2
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... ( M + N ) ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ n e. ( 0 ... ( M + N ) ) sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) )
44 3 nn0cnd
 |-  ( ph -> M e. CC )
45 44 ad2antrr
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> M e. CC )
46 4 nn0cnd
 |-  ( ph -> N e. CC )
47 46 ad2antrr
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> N e. CC )
48 elfznn0
 |-  ( k e. ( 0 ... M ) -> k e. NN0 )
49 48 adantl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> k e. NN0 )
50 49 nn0cnd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> k e. CC )
51 45 47 50 addsubd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( M + N ) - k ) = ( ( M - k ) + N ) )
52 fznn0sub
 |-  ( k e. ( 0 ... M ) -> ( M - k ) e. NN0 )
53 52 adantl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( M - k ) e. NN0 )
54 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
55 53 54 eleqtrdi
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( M - k ) e. ( ZZ>= ` 0 ) )
56 4 nn0zd
 |-  ( ph -> N e. ZZ )
57 56 ad2antrr
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> N e. ZZ )
58 eluzadd
 |-  ( ( ( M - k ) e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( ( M - k ) + N ) e. ( ZZ>= ` ( 0 + N ) ) )
59 55 57 58 syl2anc
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( M - k ) + N ) e. ( ZZ>= ` ( 0 + N ) ) )
60 51 59 eqeltrd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( M + N ) - k ) e. ( ZZ>= ` ( 0 + N ) ) )
61 47 addid2d
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( 0 + N ) = N )
62 61 fveq2d
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ZZ>= ` ( 0 + N ) ) = ( ZZ>= ` N ) )
63 60 62 eleqtrd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( M + N ) - k ) e. ( ZZ>= ` N ) )
64 fzss2
 |-  ( ( ( M + N ) - k ) e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... ( ( M + N ) - k ) ) )
65 63 64 syl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( 0 ... N ) C_ ( 0 ... ( ( M + N ) - k ) ) )
66 48 31 sylan2
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
67 66 adantr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
68 elfznn0
 |-  ( n e. ( 0 ... N ) -> n e. NN0 )
69 68 38 sylan2
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... N ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
70 69 adantlr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... N ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
71 67 70 mulcld
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... N ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
72 eldifn
 |-  ( n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) -> -. n e. ( 0 ... N ) )
73 72 adantl
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> -. n e. ( 0 ... N ) )
74 eldifi
 |-  ( n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) -> n e. ( 0 ... ( ( M + N ) - k ) ) )
75 74 33 syl
 |-  ( n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) -> n e. NN0 )
76 75 adantl
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> n e. NN0 )
77 peano2nn0
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
78 4 77 syl
 |-  ( ph -> ( N + 1 ) e. NN0 )
79 78 54 eleqtrdi
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
80 uzsplit
 |-  ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
81 79 80 syl
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
82 54 81 syl5eq
 |-  ( ph -> NN0 = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
83 ax-1cn
 |-  1 e. CC
84 pncan
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
85 46 83 84 sylancl
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
86 85 oveq2d
 |-  ( ph -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
87 86 uneq1d
 |-  ( ph -> ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
88 82 87 eqtrd
 |-  ( ph -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
89 88 ad3antrrr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
90 76 89 eleqtrd
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> n e. ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
91 elun
 |-  ( n e. ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) <-> ( n e. ( 0 ... N ) \/ n e. ( ZZ>= ` ( N + 1 ) ) ) )
92 90 91 sylib
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( n e. ( 0 ... N ) \/ n e. ( ZZ>= ` ( N + 1 ) ) ) )
93 92 ord
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( -. n e. ( 0 ... N ) -> n e. ( ZZ>= ` ( N + 1 ) ) ) )
94 73 93 mpd
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> n e. ( ZZ>= ` ( N + 1 ) ) )
95 6 ffund
 |-  ( ph -> Fun B )
96 ssun2
 |-  ( ZZ>= ` ( N + 1 ) ) C_ ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) )
97 96 82 sseqtrrid
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ NN0 )
98 6 fdmd
 |-  ( ph -> dom B = NN0 )
99 97 98 sseqtrrd
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ dom B )
100 funfvima2
 |-  ( ( Fun B /\ ( ZZ>= ` ( N + 1 ) ) C_ dom B ) -> ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` n ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
101 95 99 100 syl2anc
 |-  ( ph -> ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` n ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
102 101 ad3antrrr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` n ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
103 94 102 mpd
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( B ` n ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) )
104 8 ad3antrrr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
105 103 104 eleqtrd
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( B ` n ) e. { 0 } )
106 elsni
 |-  ( ( B ` n ) e. { 0 } -> ( B ` n ) = 0 )
107 105 106 syl
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( B ` n ) = 0 )
108 107 oveq1d
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) = ( 0 x. ( z ^ n ) ) )
109 simplr
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> z e. CC )
110 109 75 36 syl2an
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( z ^ n ) e. CC )
111 110 mul02d
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( 0 x. ( z ^ n ) ) = 0 )
112 108 111 eqtrd
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) = 0 )
113 112 oveq2d
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) x. 0 ) )
114 66 adantr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
115 114 mul01d
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. 0 ) = 0 )
116 113 115 eqtrd
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = 0 )
117 fzfid
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( 0 ... ( ( M + N ) - k ) ) e. Fin )
118 65 71 116 117 fsumss
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> sum_ n e. ( 0 ... N ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
119 118 sumeq2dv
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) sum_ n e. ( 0 ... N ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ k e. ( 0 ... M ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
120 fzfid
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... M ) e. Fin )
121 fzfid
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... N ) e. Fin )
122 120 121 66 69 fsum2mul
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) sum_ n e. ( 0 ... N ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) ) )
123 44 46 addcomd
 |-  ( ph -> ( M + N ) = ( N + M ) )
124 4 54 eleqtrdi
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
125 3 nn0zd
 |-  ( ph -> M e. ZZ )
126 eluzadd
 |-  ( ( N e. ( ZZ>= ` 0 ) /\ M e. ZZ ) -> ( N + M ) e. ( ZZ>= ` ( 0 + M ) ) )
127 124 125 126 syl2anc
 |-  ( ph -> ( N + M ) e. ( ZZ>= ` ( 0 + M ) ) )
128 44 addid2d
 |-  ( ph -> ( 0 + M ) = M )
129 128 fveq2d
 |-  ( ph -> ( ZZ>= ` ( 0 + M ) ) = ( ZZ>= ` M ) )
130 127 129 eleqtrd
 |-  ( ph -> ( N + M ) e. ( ZZ>= ` M ) )
131 123 130 eqeltrd
 |-  ( ph -> ( M + N ) e. ( ZZ>= ` M ) )
132 fzss2
 |-  ( ( M + N ) e. ( ZZ>= ` M ) -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
133 131 132 syl
 |-  ( ph -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
134 133 adantr
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
135 66 adantr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
136 39 adantlr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
137 135 136 mulcld
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
138 117 137 fsumcl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
139 eldifn
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> -. k e. ( 0 ... M ) )
140 139 adantl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> -. k e. ( 0 ... M ) )
141 eldifi
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> k e. ( 0 ... ( M + N ) ) )
142 141 26 syl
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> k e. NN0 )
143 142 adantl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> k e. NN0 )
144 peano2nn0
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
145 3 144 syl
 |-  ( ph -> ( M + 1 ) e. NN0 )
146 145 54 eleqtrdi
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` 0 ) )
147 uzsplit
 |-  ( ( M + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
148 146 147 syl
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
149 54 148 syl5eq
 |-  ( ph -> NN0 = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
150 pncan
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - 1 ) = M )
151 44 83 150 sylancl
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
152 151 oveq2d
 |-  ( ph -> ( 0 ... ( ( M + 1 ) - 1 ) ) = ( 0 ... M ) )
153 152 uneq1d
 |-  ( ph -> ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
154 149 153 eqtrd
 |-  ( ph -> NN0 = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
155 154 ad2antrr
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> NN0 = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
156 143 155 eleqtrd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> k e. ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
157 elun
 |-  ( k e. ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) <-> ( k e. ( 0 ... M ) \/ k e. ( ZZ>= ` ( M + 1 ) ) ) )
158 156 157 sylib
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( k e. ( 0 ... M ) \/ k e. ( ZZ>= ` ( M + 1 ) ) ) )
159 158 ord
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( -. k e. ( 0 ... M ) -> k e. ( ZZ>= ` ( M + 1 ) ) ) )
160 140 159 mpd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> k e. ( ZZ>= ` ( M + 1 ) ) )
161 5 ffund
 |-  ( ph -> Fun A )
162 ssun2
 |-  ( ZZ>= ` ( M + 1 ) ) C_ ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) )
163 162 149 sseqtrrid
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ NN0 )
164 5 fdmd
 |-  ( ph -> dom A = NN0 )
165 163 164 sseqtrrd
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ dom A )
166 funfvima2
 |-  ( ( Fun A /\ ( ZZ>= ` ( M + 1 ) ) C_ dom A ) -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
167 161 165 166 syl2anc
 |-  ( ph -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
168 167 ad2antrr
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
169 160 168 mpd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) )
170 7 ad2antrr
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
171 169 170 eleqtrd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) e. { 0 } )
172 elsni
 |-  ( ( A ` k ) e. { 0 } -> ( A ` k ) = 0 )
173 171 172 syl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) = 0 )
174 173 oveq1d
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
175 142 30 sylan2
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( z ^ k ) e. CC )
176 175 mul02d
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
177 174 176 eqtrd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = 0 )
178 177 adantr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = 0 )
179 178 oveq1d
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = ( 0 x. ( ( B ` n ) x. ( z ^ n ) ) ) )
180 39 adantlr
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
181 180 mul02d
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( 0 x. ( ( B ` n ) x. ( z ^ n ) ) ) = 0 )
182 179 181 eqtrd
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = 0 )
183 182 sumeq2dv
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ n e. ( 0 ... ( ( M + N ) - k ) ) 0 )
184 fzfid
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( 0 ... ( ( M + N ) - k ) ) e. Fin )
185 184 olcd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( ( 0 ... ( ( M + N ) - k ) ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... ( ( M + N ) - k ) ) e. Fin ) )
186 sumz
 |-  ( ( ( 0 ... ( ( M + N ) - k ) ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... ( ( M + N ) - k ) ) e. Fin ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) 0 = 0 )
187 185 186 syl
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) 0 = 0 )
188 183 187 eqtrd
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = 0 )
189 fzfid
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... ( M + N ) ) e. Fin )
190 134 138 188 189 fsumss
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ k e. ( 0 ... ( M + N ) ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
191 119 122 190 3eqtr3d
 |-  ( ( ph /\ z e. CC ) -> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ k e. ( 0 ... ( M + N ) ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
192 fzfid
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ( 0 ... n ) e. Fin )
193 elfznn0
 |-  ( n e. ( 0 ... ( M + N ) ) -> n e. NN0 )
194 193 37 sylan2
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ( z ^ n ) e. CC )
195 simpll
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ph )
196 elfznn0
 |-  ( k e. ( 0 ... n ) -> k e. NN0 )
197 5 ffvelrnda
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. CC )
198 195 196 197 syl2an
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( A ` k ) e. CC )
199 fznn0sub
 |-  ( k e. ( 0 ... n ) -> ( n - k ) e. NN0 )
200 6 ffvelrnda
 |-  ( ( ph /\ ( n - k ) e. NN0 ) -> ( B ` ( n - k ) ) e. CC )
201 195 199 200 syl2an
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( B ` ( n - k ) ) e. CC )
202 198 201 mulcld
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) e. CC )
203 192 194 202 fsummulc1
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) )
204 simplr
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> z e. CC )
205 204 196 29 syl2an
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( z ^ k ) e. CC )
206 expcl
 |-  ( ( z e. CC /\ ( n - k ) e. NN0 ) -> ( z ^ ( n - k ) ) e. CC )
207 204 199 206 syl2an
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( z ^ ( n - k ) ) e. CC )
208 198 205 201 207 mul4d
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) = ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( ( z ^ k ) x. ( z ^ ( n - k ) ) ) ) )
209 204 adantr
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> z e. CC )
210 199 adantl
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( n - k ) e. NN0 )
211 196 adantl
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> k e. NN0 )
212 209 210 211 expaddd
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( z ^ ( k + ( n - k ) ) ) = ( ( z ^ k ) x. ( z ^ ( n - k ) ) ) )
213 211 nn0cnd
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> k e. CC )
214 193 ad2antlr
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> n e. NN0 )
215 214 nn0cnd
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> n e. CC )
216 213 215 pncan3d
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( k + ( n - k ) ) = n )
217 216 oveq2d
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( z ^ ( k + ( n - k ) ) ) = ( z ^ n ) )
218 212 217 eqtr3d
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( z ^ k ) x. ( z ^ ( n - k ) ) ) = ( z ^ n ) )
219 218 oveq2d
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( ( z ^ k ) x. ( z ^ ( n - k ) ) ) ) = ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) )
220 208 219 eqtrd
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) = ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) )
221 220 sumeq2dv
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) = sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) )
222 203 221 eqtr4d
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) )
223 222 sumeq2dv
 |-  ( ( ph /\ z e. CC ) -> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = sum_ n e. ( 0 ... ( M + N ) ) sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) )
224 43 191 223 3eqtr4rd
 |-  ( ( ph /\ z e. CC ) -> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) ) )
225 fveq2
 |-  ( n = k -> ( B ` n ) = ( B ` k ) )
226 oveq2
 |-  ( n = k -> ( z ^ n ) = ( z ^ k ) )
227 225 226 oveq12d
 |-  ( n = k -> ( ( B ` n ) x. ( z ^ n ) ) = ( ( B ` k ) x. ( z ^ k ) ) )
228 227 cbvsumv
 |-  sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) = sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) )
229 228 oveq2i
 |-  ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) )
230 224 229 eqtrdi
 |-  ( ( ph /\ z e. CC ) -> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
231 230 mpteq2dva
 |-  ( ph -> ( z e. CC |-> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) ) = ( z e. CC |-> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ) )
232 17 231 eqtr4d
 |-  ( 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 ) ) ) )