ply1mulgsumlem3

	Ref	Expression
Hypotheses	ply1mulgsum.p	$⊢ P = {Poly}_{1} (R)$
	ply1mulgsum.b	$⊢ B = {Base}_{P}$
	ply1mulgsum.a	$⊢ A = {coe}_{1} (K)$
	ply1mulgsum.c	$⊢ C = {coe}_{1} (L)$
	ply1mulgsum.x	$⊢ X = {var}_{1} (R)$
	ply1mulgsum.pm	$⊢ \underset{˙}{\times} = \cdot_{P}$
	ply1mulgsum.sm	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	ply1mulgsum.rm	$⊢ \underset{˙}{*} = \cdot_{R}$
	ply1mulgsum.m	$⊢ M = {mulGrp}_{P}$
	ply1mulgsum.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
Assertion	ply1mulgsumlem3	$⊢ (R \in Ring \land K \in B \land L \in B) \to {finSupp}_{0_{R}} ((k \in ℕ_{0} ⟼ {\sum_{R}}_{l = 0}^{k} (A (l) \underset{˙}{*} C (k - l))))$

Proof

Step	Hyp	Ref	Expression
1		ply1mulgsum.p	$⊢ P = {Poly}_{1} (R)$
2		ply1mulgsum.b	$⊢ B = {Base}_{P}$
3		ply1mulgsum.a	$⊢ A = {coe}_{1} (K)$
4		ply1mulgsum.c	$⊢ C = {coe}_{1} (L)$
5		ply1mulgsum.x	$⊢ X = {var}_{1} (R)$
6		ply1mulgsum.pm	$⊢ \underset{˙}{\times} = \cdot_{P}$
7		ply1mulgsum.sm	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
8		ply1mulgsum.rm	$⊢ \underset{˙}{*} = \cdot_{R}$
9		ply1mulgsum.m	$⊢ M = {mulGrp}_{P}$
10		ply1mulgsum.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
11		fvexd	$⊢ (R \in Ring \land K \in B \land L \in B) \to 0_{R} \in V$
12		ovexd	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to {\sum_{R}}_{l = 0}^{k} (A (l) \underset{˙}{*} C (k - l)) \in V$
13	1 2 3 4 5 6 7 8 9 10	ply1mulgsumlem2	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{*} C (n - l)) = 0_{R})$
14		vex	$⊢ n \in V$
15		csbov2g	$⊢ n \in V \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) = \sum_{R} ⦋ n / k ⦌ (l \in (0 \dots k) ⟼ A (l) \underset{˙}{} C (k - l))$
16		id	$⊢ n \in V \to n \in V$
17		oveq2	$⊢ k = n \to (0 \dots k) = (0 \dots n)$
18		fvoveq1	$⊢ k = n \to C (k - l) = C (n - l)$
19	18	oveq2d	$⊢ k = n \to A (l) \underset{˙}{} C (k - l) = A (l) \underset{˙}{} C (n - l)$
20	17 19	mpteq12dv	$⊢ k = n \to (l \in (0 \dots k) ⟼ A (l) \underset{˙}{} C (k - l)) = (l \in (0 \dots n) ⟼ A (l) \underset{˙}{} C (n - l))$
21	20	adantl	$⊢ (n \in V \land k = n) \to (l \in (0 \dots k) ⟼ A (l) \underset{˙}{} C (k - l)) = (l \in (0 \dots n) ⟼ A (l) \underset{˙}{} C (n - l))$
22	16 21	csbied	$⊢ n \in V \to ⦋ n / k ⦌ (l \in (0 \dots k) ⟼ A (l) \underset{˙}{} C (k - l)) = (l \in (0 \dots n) ⟼ A (l) \underset{˙}{} C (n - l))$
23	22	oveq2d	$⊢ n \in V \to \sum_{R} ⦋ n / k ⦌ (l \in (0 \dots k) ⟼ A (l) \underset{˙}{} C (k - l)) = {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l))$
24	15 23	eqtrd	$⊢ n \in V \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) = {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l))$
25	14 24	ax-mp	$⊢ ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) = {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l))$
26		simpr	$⊢ ((((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \land {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}) \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}$
27	25 26	syl5eq	$⊢ ((((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \land {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}) \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) = 0_{R}$
28	27	ex	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to ({\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R} \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) = 0_{R})$
29	28	imim2d	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to ((s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}) \to (s < n \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) = 0_{R}))$
30	29	ralimdva	$⊢ ((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \to (\forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}) \to \forall n \in ℕ_{0} (s < n \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) = 0_{R}))$
31	30	reximdva	$⊢ (R \in Ring \land K \in B \land L \in B) \to (\exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = 0_{R}) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) = 0_{R}))$
32	13 31	mpd	$⊢ (R \in Ring \land K \in B \land L \in B) \to \exists s \in ℕ_{0} \forall n \in ℕ_{0} (s < n \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) = 0_{R})$
33	11 12 32	mptnn0fsupp	$⊢ (R \in Ring \land K \in B \land L \in B) \to {finSupp}_{0_{R}} ((k \in ℕ_{0} ⟼ {\sum_{R}}_{l = 0}^{k} (A (l) \underset{˙}{*} C (k - l))))$

Metamath Proof Explorer

Theorem ply1mulgsumlem3

Proof