Metamath Proof Explorer

Theorem coemullem

Description: Lemma for coemul and dgrmul . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses coefv0.1 
|- A = ( coeff ` F )
coeadd.2 
|- B = ( coeff ` G )
coeadd.3 
|- M = ( deg ` F )
coeadd.4 
|- N = ( deg ` G )
Assertion coemullem 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF x. G ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) /\ ( deg ` ( F oF x. G ) ) <_ ( M + N ) ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 
 |-  A = ( coeff ` F )
2 coeadd.2 
 |-  B = ( coeff ` G )
3 coeadd.3 
 |-  M = ( deg ` F )
4 coeadd.4 
 |-  N = ( deg ` G )
5 plymulcl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF x. G ) e. ( Poly ` CC ) )
6 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
7 3 6 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> M e. NN0 )
8 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
9 4 8 eqeltrid 
 |-  ( G e. ( Poly ` S ) -> N e. NN0 )
10 nn0addcl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M + N ) e. NN0 )
11 7 9 10 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( M + N ) e. NN0 )
12 fzfid 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( 0 ... n ) e. Fin )
13 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
14 13 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> A : NN0 --> CC )
15 14 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ n e. NN0 ) -> A : NN0 --> CC )
16 elfznn0 
 |-  ( k e. ( 0 ... n ) -> k e. NN0 )
17 ffvelrn 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
18 15 16 17 syl2an 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... n ) ) -> ( A ` k ) e. CC )
19 2 coef3 
 |-  ( G e. ( Poly ` S ) -> B : NN0 --> CC )
20 19 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> B : NN0 --> CC )
21 20 ad2antrr 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... n ) ) -> B : NN0 --> CC )
22 fznn0sub 
 |-  ( k e. ( 0 ... n ) -> ( n - k ) e. NN0 )
23 22 adantl 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... n ) ) -> ( n - k ) e. NN0 )
24 21 23 ffvelrnd 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... n ) ) -> ( B ` ( n - k ) ) e. CC )
25 18 24 mulcld 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ n e. NN0 ) /\ k e. ( 0 ... n ) ) -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) e. CC )
26 12 25 fsumcl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ n e. NN0 ) -> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) e. CC )
27 26 fmpttd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) : NN0 --> CC )
28 oveq2 
 |-  ( n = j -> ( 0 ... n ) = ( 0 ... j ) )
29 fvoveq1 
 |-  ( n = j -> ( B ` ( n - k ) ) = ( B ` ( j - k ) ) )
30 29 oveq2d 
 |-  ( n = j -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) = ( ( A ` k ) x. ( B ` ( j - k ) ) ) )
31 30 adantr 
 |-  ( ( n = j /\ k e. ( 0 ... n ) ) -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) = ( ( A ` k ) x. ( B ` ( j - k ) ) ) )
32 28 31 sumeq12dv 
 |-  ( n = j -> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) = sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) )
33 eqid 
 |-  ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) )
34 sumex 
 |-  sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) e. _V
35 32 33 34 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) = sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) )
36 35 ad2antrl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) = sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) )
37 simp2r 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> -. j <_ ( M + N ) )
38 simp2l 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> j e. NN0 )
39 38 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> j e. RR )
40 simp3l 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> k e. ( 0 ... j ) )
41 elfznn0 
 |-  ( k e. ( 0 ... j ) -> k e. NN0 )
42 40 41 syl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> k e. NN0 )
43 42 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> k e. RR )
44 9 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> N e. NN0 )
45 44 3ad2ant1 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> N e. NN0 )
46 45 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> N e. RR )
47 39 43 46 lesubadd2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( ( j - k ) <_ N <-> j <_ ( k + N ) ) )
48 7 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> M e. NN0 )
49 48 3ad2ant1 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> M e. NN0 )
50 49 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> M e. RR )
51 simp3r 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> k <_ M )
52 43 50 46 51 leadd1dd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( k + N ) <_ ( M + N ) )
53 43 46 readdcld 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( k + N ) e. RR )
54 50 46 readdcld 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( M + N ) e. RR )
55 letr 
 |-  ( ( j e. RR /\ ( k + N ) e. RR /\ ( M + N ) e. RR ) -> ( ( j <_ ( k + N ) /\ ( k + N ) <_ ( M + N ) ) -> j <_ ( M + N ) ) )
56 39 53 54 55 syl3anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( ( j <_ ( k + N ) /\ ( k + N ) <_ ( M + N ) ) -> j <_ ( M + N ) ) )
57 52 56 mpan2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( j <_ ( k + N ) -> j <_ ( M + N ) ) )
58 47 57 sylbid 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( ( j - k ) <_ N -> j <_ ( M + N ) ) )
59 37 58 mtod 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> -. ( j - k ) <_ N )
60 simpr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G e. ( Poly ` S ) )
61 60 3ad2ant1 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> G e. ( Poly ` S ) )
62 fznn0sub 
 |-  ( k e. ( 0 ... j ) -> ( j - k ) e. NN0 )
63 40 62 syl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( j - k ) e. NN0 )
64 2 4 dgrub 
 |-  ( ( G e. ( Poly ` S ) /\ ( j - k ) e. NN0 /\ ( B ` ( j - k ) ) =/= 0 ) -> ( j - k ) <_ N )
65 64 3expia 
 |-  ( ( G e. ( Poly ` S ) /\ ( j - k ) e. NN0 ) -> ( ( B ` ( j - k ) ) =/= 0 -> ( j - k ) <_ N ) )
66 61 63 65 syl2anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( ( B ` ( j - k ) ) =/= 0 -> ( j - k ) <_ N ) )
67 66 necon1bd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( -. ( j - k ) <_ N -> ( B ` ( j - k ) ) = 0 ) )
68 59 67 mpd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( B ` ( j - k ) ) = 0 )
69 68 oveq2d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( ( A ` k ) x. ( B ` ( j - k ) ) ) = ( ( A ` k ) x. 0 ) )
70 14 3ad2ant1 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> A : NN0 --> CC )
71 70 42 ffvelrnd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( A ` k ) e. CC )
72 71 mul01d 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( ( A ` k ) x. 0 ) = 0 )
73 69 72 eqtrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) /\ ( k e. ( 0 ... j ) /\ k <_ M ) ) -> ( ( A ` k ) x. ( B ` ( j - k ) ) ) = 0 )
74 73 3expia 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) -> ( ( k e. ( 0 ... j ) /\ k <_ M ) -> ( ( A ` k ) x. ( B ` ( j - k ) ) ) = 0 ) )
75 74 impl 
 |-  ( ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) /\ k <_ M ) -> ( ( A ` k ) x. ( B ` ( j - k ) ) ) = 0 )
76 simpl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F e. ( Poly ` S ) )
77 76 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) -> F e. ( Poly ` S ) )
78 1 3 dgrub 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 /\ ( A ` k ) =/= 0 ) -> k <_ M )
79 78 3expia 
 |-  ( ( F e. ( Poly ` S ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ M ) )
80 77 41 79 syl2an 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) -> ( ( A ` k ) =/= 0 -> k <_ M ) )
81 80 necon1bd 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) -> ( -. k <_ M -> ( A ` k ) = 0 ) )
82 81 imp 
 |-  ( ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) /\ -. k <_ M ) -> ( A ` k ) = 0 )
83 82 oveq1d 
 |-  ( ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) /\ -. k <_ M ) -> ( ( A ` k ) x. ( B ` ( j - k ) ) ) = ( 0 x. ( B ` ( j - k ) ) ) )
84 20 ad3antrrr 
 |-  ( ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) /\ -. k <_ M ) -> B : NN0 --> CC )
85 62 ad2antlr 
 |-  ( ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) /\ -. k <_ M ) -> ( j - k ) e. NN0 )
86 84 85 ffvelrnd 
 |-  ( ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) /\ -. k <_ M ) -> ( B ` ( j - k ) ) e. CC )
87 86 mul02d 
 |-  ( ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) /\ -. k <_ M ) -> ( 0 x. ( B ` ( j - k ) ) ) = 0 )
88 83 87 eqtrd 
 |-  ( ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) /\ -. k <_ M ) -> ( ( A ` k ) x. ( B ` ( j - k ) ) ) = 0 )
89 75 88 pm2.61dan 
 |-  ( ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) /\ k e. ( 0 ... j ) ) -> ( ( A ` k ) x. ( B ` ( j - k ) ) ) = 0 )
90 89 sumeq2dv 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) -> sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) = sum_ k e. ( 0 ... j ) 0 )
91 fzfi 
 |-  ( 0 ... j ) e. Fin
92 91 olci 
 |-  ( ( 0 ... j ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... j ) e. Fin )
93 sumz 
 |-  ( ( ( 0 ... j ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... j ) e. Fin ) -> sum_ k e. ( 0 ... j ) 0 = 0 )
94 92 93 ax-mp 
 |-  sum_ k e. ( 0 ... j ) 0 = 0
95 90 94 eqtrdi 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) -> sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) = 0 )
96 36 95 eqtrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ ( j e. NN0 /\ -. j <_ ( M + N ) ) ) -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) = 0 )
97 96 expr 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ j e. NN0 ) -> ( -. j <_ ( M + N ) -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) = 0 ) )
98 97 necon1ad 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ j e. NN0 ) -> ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) =/= 0 -> j <_ ( M + N ) ) )
99 98 ralrimiva 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> A. j e. NN0 ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) =/= 0 -> j <_ ( M + N ) ) )
100 plyco0 
 |-  ( ( ( M + N ) e. NN0 /\ ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) : NN0 --> CC ) -> ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) " ( ZZ>= ` ( ( M + N ) + 1 ) ) ) = { 0 } <-> A. j e. NN0 ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) =/= 0 -> j <_ ( M + N ) ) ) )
101 11 27 100 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) " ( ZZ>= ` ( ( M + N ) + 1 ) ) ) = { 0 } <-> A. j e. NN0 ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) =/= 0 -> j <_ ( M + N ) ) ) )
102 99 101 mpbird 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) " ( ZZ>= ` ( ( M + N ) + 1 ) ) ) = { 0 } )
103 1 3 dgrub2 
 |-  ( F e. ( Poly ` S ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
104 103 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
105 2 4 dgrub2 
 |-  ( G e. ( Poly ` S ) -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
106 105 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
107 1 3 coeid 
 |-  ( F e. ( Poly ` S ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
108 107 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
109 2 4 coeid 
 |-  ( G e. ( Poly ` S ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
110 109 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
111 76 60 48 44 14 20 104 106 108 110 plymullem1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF x. G ) = ( z e. CC |-> sum_ j e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) x. ( z ^ j ) ) ) )
112 elfznn0 
 |-  ( j e. ( 0 ... ( M + N ) ) -> j e. NN0 )
113 112 35 syl 
 |-  ( j e. ( 0 ... ( M + N ) ) -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) = sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) )
114 113 oveq1d 
 |-  ( j e. ( 0 ... ( M + N ) ) -> ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) x. ( z ^ j ) ) = ( sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) x. ( z ^ j ) ) )
115 114 sumeq2i 
 |-  sum_ j e. ( 0 ... ( M + N ) ) ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) x. ( z ^ j ) ) = sum_ j e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) x. ( z ^ j ) )
116 115 mpteq2i 
 |-  ( z e. CC |-> sum_ j e. ( 0 ... ( M + N ) ) ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) x. ( z ^ j ) ) ) = ( z e. CC |-> sum_ j e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... j ) ( ( A ` k ) x. ( B ` ( j - k ) ) ) x. ( z ^ j ) ) )
117 111 116 eqtr4di 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF x. G ) = ( z e. CC |-> sum_ j e. ( 0 ... ( M + N ) ) ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) x. ( z ^ j ) ) ) )
118 5 11 27 102 117 coeeq 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( coeff ` ( F oF x. G ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) )
119 ffvelrn 
 |-  ( ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) : NN0 --> CC /\ j e. NN0 ) -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) e. CC )
120 27 112 119 syl2an 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) /\ j e. ( 0 ... ( M + N ) ) ) -> ( ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) ` j ) e. CC )
121 5 11 120 117 dgrle 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF x. G ) ) <_ ( M + N ) )
122 118 121 jca 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF x. G ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) ) /\ ( deg ` ( F oF x. G ) ) <_ ( M + N ) ) )