Metamath Proof Explorer

Theorem coemul

Description: A coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses coefv0.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
coeadd.2 ⊢ 𝐵 = ( coeff ‘ 𝐺 )
Assertion coemul ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 coeadd.2 ⊢ 𝐵 = ( coeff ‘ 𝐺 )
3 eqid ⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
4 eqid ⊢ ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 )
5 1 2 3 4 coemullem ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ∧ ( deg ‘ ( 𝐹 ∘f · 𝐺 ) ) ≤ ( ( deg ‘ 𝐹 ) + ( deg ‘ 𝐺 ) ) ) )
6 5 simpld ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) )
7 6 fveq1d ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝑁 ) = ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑁 ) )
8 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
9 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) = ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) )
10 9 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) ) )
11 10 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) ) )
12 8 11 sumeq12dv ⊢ ( 𝑛 = 𝑁 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) ) )
13 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) )
14 sumex ⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) ) ∈ V
15 12 13 14 fvmpt ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑛 − 𝑘 ) ) ) ) ‘ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) ) )
16 7 15 sylan9eq ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) ) )
17 16 3impa ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐹 ∘f · 𝐺 ) ) ‘ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝐵 ‘ ( 𝑁 − 𝑘 ) ) ) )