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 ⊢ A = coeff ⁡ F
coeadd.2 ⊢ B = coeff ⁡ G
Assertion coemul ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S ∧ N ∈ ℕ 0 → coeff ⁡ F × f G ⁡ N = ∑ k = 0 N A ⁡ k ⁢ B ⁡ N − k

Proof

Step Hyp Ref Expression
1 coefv0.1 ⊢ A = coeff ⁡ F
2 coeadd.2 ⊢ B = coeff ⁡ G
3 eqid ⊢ deg ⁡ F = deg ⁡ F
4 eqid ⊢ deg ⁡ G = deg ⁡ G
5 1 2 3 4 coemullem ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ F × f G = n ∈ ℕ 0 ⟼ ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k ∧ deg ⁡ F × f G ≤ deg ⁡ F + deg ⁡ G
6 5 simpld ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ F × f G = n ∈ ℕ 0 ⟼ ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k
7 6 fveq1d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ F × f G ⁡ N = n ∈ ℕ 0 ⟼ ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k ⁡ N
8 oveq2 ⊢ n = N → 0 … n = 0 … N
9 fvoveq1 ⊢ n = N → B ⁡ n − k = B ⁡ N − k
10 9 oveq2d ⊢ n = N → A ⁡ k ⁢ B ⁡ n − k = A ⁡ k ⁢ B ⁡ N − k
11 10 adantr ⊢ n = N ∧ k ∈ 0 … n → A ⁡ k ⁢ B ⁡ n − k = A ⁡ k ⁢ B ⁡ N − k
12 8 11 sumeq12dv ⊢ n = N → ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k = ∑ k = 0 N A ⁡ k ⁢ B ⁡ N − k
13 eqid ⊢ n ∈ ℕ 0 ⟼ ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k = n ∈ ℕ 0 ⟼ ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k
14 sumex ⊢ ∑ k = 0 N A ⁡ k ⁢ B ⁡ N − k ∈ V
15 12 13 14 fvmpt ⊢ N ∈ ℕ 0 → n ∈ ℕ 0 ⟼ ∑ k = 0 n A ⁡ k ⁢ B ⁡ n − k ⁡ N = ∑ k = 0 N A ⁡ k ⁢ B ⁡ N − k
16 7 15 sylan9eq ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S ∧ N ∈ ℕ 0 → coeff ⁡ F × f G ⁡ N = ∑ k = 0 N A ⁡ k ⁢ B ⁡ N − k
17 16 3impa ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S ∧ N ∈ ℕ 0 → coeff ⁡ F × f G ⁡ N = ∑ k = 0 N A ⁡ k ⁢ B ⁡ N − k