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 \in Poly (S) \land G \in Poly (S) \land N \in ℕ_{0}) \to coeff (F \times_{f} G) (N) = \sum_{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 \in Poly (S) \land G \in Poly (S)) \to (coeff (F \times_{f} G) = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) \land \deg (F \times_{f} G) \leq \deg (F) + \deg (G))$
6	5	simpld	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F \times_{f} G) = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k))$
7	6	fveq1d	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to coeff (F \times_{f} G) (N) = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (N)$
8		oveq2	$⊢ n = N \to (0 \dots n) = (0 \dots N)$
9		fvoveq1	$⊢ n = N \to B (n - k) = B (N - k)$
10	9	oveq2d	$⊢ n = N \to A (k) B (n - k) = A (k) B (N - k)$
11	10	adantr	$⊢ (n = N \land k \in (0 \dots n)) \to A (k) B (n - k) = A (k) B (N - k)$
12	8 11	sumeq12dv	$⊢ n = N \to \sum_{k = 0}^{n} A (k) B (n - k) = \sum_{k = 0}^{N} A (k) B (N - k)$
13		eqid	$⊢ (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) = (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k))$
14		sumex	$⊢ \sum_{k = 0}^{N} A (k) B (N - k) \in V$
15	12 13 14	fvmpt	$⊢ N \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \sum_{k = 0}^{n} A (k) B (n - k)) (N) = \sum_{k = 0}^{N} A (k) B (N - k)$
16	7 15	sylan9eq	$⊢ ((F \in Poly (S) \land G \in Poly (S)) \land N \in ℕ_{0}) \to coeff (F \times_{f} G) (N) = \sum_{k = 0}^{N} A (k) B (N - k)$
17	16	3impa	$⊢ (F \in Poly (S) \land G \in Poly (S) \land N \in ℕ_{0}) \to coeff (F \times_{f} G) (N) = \sum_{k = 0}^{N} A (k) B (N - k)$