Metamath Proof Explorer

Theorem coemullem

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

Ref Expression
Hypotheses coefv0.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
coeadd.2 ⊢ 𝐵 = ( coeff ‘ 𝐺 )
coeadd.3 ⊢ 𝑀 = ( deg ‘ 𝐹 )
coeadd.4 ⊢ 𝑁 = ( deg ‘ 𝐺 )
Assertion coemullem ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ∧ ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 coeadd.2 ⊢ 𝐵 = ( coeff ‘ 𝐺 )
3 coeadd.3 ⊢ 𝑀 = ( deg ‘ 𝐹 )
4 coeadd.4 ⊢ 𝑁 = ( deg ‘ 𝐺 )
5 plymulcl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) )
6 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
7 3 6 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑀 ∈ ℕ0 )
8 dgrcl ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
9 4 8 eqeltrid ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
10 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
11 7 9 10 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
12 fzfid ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 0 ... 𝑛 ) ∈ Fin )
13 1 coef3 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
14 13 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
15 14 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐴 : ℕ0 ⟶ ℂ )
16 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → 𝑘 ∈ ℕ0 )
17 ffvelrn ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
18 15 16 17 syl2an ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
19 2 coef3 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐵 : ℕ0 ⟶ ℂ )
20 19 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐵 : ℕ0 ⟶ ℂ )
21 20 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → 𝐵 : ℕ0 ⟶ ℂ )
22 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑘 ) ∈ ℕ0 )
23 22 adantl ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝑛 − 𝑘 ) ∈ ℕ0 )
24 21 23 ffvelrnd ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ∈ ℂ )
25 18 24 mulcld ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ∈ ℂ )
26 12 25 fsumcl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ∈ ℂ )
27 26 fmpttd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) : ℕ0 ⟶ ℂ )
28 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 0 ... 𝑛 ) = ( 0 ... 𝑗 ) )
29 fvoveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) = ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) )
30 29 oveq2d ⊢ ( 𝑛 = 𝑗 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) )
31 30 adantr ⊢ ( ( 𝑛 = 𝑗 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) )
32 28 31 sumeq12dv ⊢ ( 𝑛 = 𝑗 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) )
33 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) )
34 sumex ⊢ Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) ∈ V
35 32 33 34 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) )
36 35 ad2antrl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) )
37 simp2r ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) )
38 simp2l ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑗 ∈ ℕ0 )
39 38 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑗 ∈ ℝ )
40 simp3l ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑘 ∈ ( 0 ... 𝑗 ) )
41 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑗 ) → 𝑘 ∈ ℕ0 )
42 40 41 syl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
43 42 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑘 ∈ ℝ )
44 9 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑁 ∈ ℕ0 )
45 44 3ad2ant1 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑁 ∈ ℕ0 )
46 45 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑁 ∈ ℝ )
47 39 43 46 lesubadd2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( ( 𝑗 − 𝑘 ) ≤ 𝑁 ↔ 𝑗 ≤ ( 𝑘 + 𝑁 ) ) )
48 7 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝑀 ∈ ℕ0 )
49 48 3ad2ant1 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑀 ∈ ℕ0 )
50 49 nn0red ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑀 ∈ ℝ )
51 simp3r ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝑘 ≤ 𝑀 )
52 43 50 46 51 leadd1dd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( 𝑘 + 𝑁 ) ≤ ( 𝑀 + 𝑁 ) )
53 43 46 readdcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( 𝑘 + 𝑁 ) ∈ ℝ )
54 50 46 readdcld ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
55 letr ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 𝑘 + 𝑁 ) ∈ ℝ ∧ ( 𝑀 + 𝑁 ) ∈ ℝ ) → ( ( 𝑗 ≤ ( 𝑘 + 𝑁 ) ∧ ( 𝑘 + 𝑁 ) ≤ ( 𝑀 + 𝑁 ) ) → 𝑗 ≤ ( 𝑀 + 𝑁 ) ) )
56 39 53 54 55 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( ( 𝑗 ≤ ( 𝑘 + 𝑁 ) ∧ ( 𝑘 + 𝑁 ) ≤ ( 𝑀 + 𝑁 ) ) → 𝑗 ≤ ( 𝑀 + 𝑁 ) ) )
57 52 56 mpan2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( 𝑗 ≤ ( 𝑘 + 𝑁 ) → 𝑗 ≤ ( 𝑀 + 𝑁 ) ) )
58 47 57 sylbid ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( ( 𝑗 − 𝑘 ) ≤ 𝑁 → 𝑗 ≤ ( 𝑀 + 𝑁 ) ) )
59 37 58 mtod ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ¬ ( 𝑗 − 𝑘 ) ≤ 𝑁 )
60 simpr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
61 60 3ad2ant1 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
62 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... 𝑗 ) → ( 𝑗 − 𝑘 ) ∈ ℕ0 )
63 40 62 syl ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( 𝑗 − 𝑘 ) ∈ ℕ0 )
64 2 4 dgrub ⊢ ( ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑗 − 𝑘 ) ∈ ℕ0 ∧ ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ≠ 0 ) → ( 𝑗 − 𝑘 ) ≤ 𝑁 )
65 64 3expia ⊢ ( ( 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ ( 𝑗 − 𝑘 ) ∈ ℕ0 ) → ( ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ≠ 0 → ( 𝑗 − 𝑘 ) ≤ 𝑁 ) )
66 61 63 65 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ≠ 0 → ( 𝑗 − 𝑘 ) ≤ 𝑁 ) )
67 66 necon1bd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( ¬ ( 𝑗 − 𝑘 ) ≤ 𝑁 → ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) = 0 ) )
68 59 67 mpd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) = 0 )
69 68 oveq2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · 0 ) )
70 14 3ad2ant1 ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
71 70 42 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
72 71 mul01d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( ( 𝐴 ‘ 𝑘 ) · 0 ) = 0 )
73 69 72 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = 0 )
74 73 3expia ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑘 ∈ ( 0 ... 𝑗 ) ∧ 𝑘 ≤ 𝑀 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = 0 ) )
75 74 impl ⊢ ( ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) ∧ 𝑘 ≤ 𝑀 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = 0 )
76 simpl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
77 76 adantr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
78 1 3 dgrub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑀 )
79 78 3expia ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
80 77 41 79 syl2an ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑀 ) )
81 80 necon1bd ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( ¬ 𝑘 ≤ 𝑀 → ( 𝐴 ‘ 𝑘 ) = 0 ) )
82 81 imp ⊢ ( ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( 𝐴 ‘ 𝑘 ) = 0 )
83 82 oveq1d ⊢ ( ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = ( 0 · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) )
84 20 ad3antrrr ⊢ ( ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → 𝐵 : ℕ0 ⟶ ℂ )
85 62 ad2antlr ⊢ ( ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( 𝑗 − 𝑘 ) ∈ ℕ0 )
86 84 85 ffvelrnd ⊢ ( ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ∈ ℂ )
87 86 mul02d ⊢ ( ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( 0 · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = 0 )
88 83 87 eqtrd ⊢ ( ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) ∧ ¬ 𝑘 ≤ 𝑀 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = 0 )
89 75 88 pm2.61dan ⊢ ( ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = 0 )
90 89 sumeq2dv ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) → Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) 0 )
91 fzfi ⊢ ( 0 ... 𝑗 ) ∈ Fin
92 91 olci ⊢ ( ( 0 ... 𝑗 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑗 ) ∈ Fin )
93 sumz ⊢ ( ( ( 0 ... 𝑗 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑗 ) ∈ Fin ) → Σ 𝑘 ∈ ( 0 ... 𝑗 ) 0 = 0 )
94 92 93 ax-mp ⊢ Σ 𝑘 ∈ ( 0 ... 𝑗 ) 0 = 0
95 90 94 eqtrdi ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) → Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) = 0 )
96 36 95 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ ( 𝑗 ∈ ℕ0 ∧ ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) = 0 )
97 96 expr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑗 ∈ ℕ0 ) → ( ¬ 𝑗 ≤ ( 𝑀 + 𝑁 ) → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) = 0 ) )
98 97 necon1ad ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑗 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) ≠ 0 → 𝑗 ≤ ( 𝑀 + 𝑁 ) ) )
99 98 ralrimiva ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ∀ 𝑗 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) ≠ 0 → 𝑗 ≤ ( 𝑀 + 𝑁 ) ) )
100 plyco0 ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) “ ( ℤ≥ ‘ ( ( 𝑀 + 𝑁 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑗 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) ≠ 0 → 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) )
101 11 27 100 syl2anc ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) “ ( ℤ≥ ‘ ( ( 𝑀 + 𝑁 ) + 1 ) ) ) = { 0 } ↔ ∀ 𝑗 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) ≠ 0 → 𝑗 ≤ ( 𝑀 + 𝑁 ) ) ) )
102 99 101 mpbird ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) “ ( ℤ≥ ‘ ( ( 𝑀 + 𝑁 ) + 1 ) ) ) = { 0 } )
103 1 3 dgrub2 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
104 103 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
105 2 4 dgrub2 ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
106 105 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
107 1 3 coeid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
108 107 adantr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
109 2 4 coeid ⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
110 109 adantl ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
111 76 60 48 44 14 20 104 106 108 110 plymullem1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f · 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) · ( 𝑧 ↑ 𝑗 ) ) ) )
112 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → 𝑗 ∈ ℕ0 )
113 112 35 syl ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) )
114 113 oveq1d ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) · ( 𝑧 ↑ 𝑗 ) ) )
115 114 sumeq2i ⊢ Σ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) · ( 𝑧 ↑ 𝑗 ) )
116 115 mpteq2i ⊢ ( 𝑧 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑗 − 𝑘 ) ) ) · ( 𝑧 ↑ 𝑗 ) ) )
117 111 116 eqtr4di ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f · 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) · ( 𝑧 ↑ 𝑗 ) ) ) )
118 5 11 27 102 117 coeeq ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) )
119 ffvelrn ⊢ ( ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) : ℕ0 ⟶ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) ∈ ℂ )
120 27 112 119 syl2an ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑗 ) ∈ ℂ )
121 5 11 120 117 dgrle ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) )
122 118 121 jca ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ∧ ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) ) )