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		ffvelcdm	⊢ ( ( 𝐴 : ℕ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	ffvelcdmd	⊢ ( ( ( ( 𝐹 ∈ ( 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	ffvelcdmd	⊢ ( ( ( 𝐹 ∈ ( 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	ffvelcdmd	⊢ ( ( ( ( ( 𝐹 ∈ ( 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		ffvelcdm	⊢ ( ( ( 𝑛 ∈ ℕ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 · 𝐺 ) ) ≤ ( 𝑀 + 𝑁 ) ) )