ply1mulgsumlem4

	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	ply1mulgsumlem4	$⊢ (R \in Ring \land K \in B \land L \in B) \to {finSupp}_{0_{P}} ((k \in ℕ_{0} ⟼ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)))$

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_{P} \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))) \underset{˙}{\cdot} (k \underset{˙}{\times} X) \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		csbov12g	$⊢ n \in V \to ⦋ n / k ⦌ (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} ⦋ n / k ⦌ (k \underset{˙}{\times} X)$
16		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))$
17		id	$⊢ n \in V \to n \in V$
18		oveq2	$⊢ k = n \to (0 \dots k) = (0 \dots n)$
19		fvoveq1	$⊢ k = n \to C (k - l) = C (n - l)$
20	19	oveq2d	$⊢ k = n \to A (l) \underset{˙}{} C (k - l) = A (l) \underset{˙}{} C (n - l)$
21	18 20	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))$
22	21	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))$
23	17 22	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))$
24	23	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))$
25	16 24	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))$
26		csbov1g	$⊢ n \in V \to ⦋ n / k ⦌ (k \underset{˙}{\times} X) = ⦋ n / k ⦌ k \underset{˙}{\times} X$
27		csbvarg	$⊢ n \in V \to ⦋ n / k ⦌ k = n$
28	27	oveq1d	$⊢ n \in V \to ⦋ n / k ⦌ k \underset{˙}{\times} X = n \underset{˙}{\times} X$
29	26 28	eqtrd	$⊢ n \in V \to ⦋ n / k ⦌ (k \underset{˙}{\times} X) = n \underset{˙}{\times} X$
30	25 29	oveq12d	$⊢ n \in V \to ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} ⦋ n / k ⦌ (k \underset{˙}{\times} X) = ({\sum_{R}}_{l = 0}^{n}, (A (l) \underset{˙}{} C (n - l))) \underset{˙}{\cdot} (n \underset{˙}{\times} X)$
31	15 30	eqtrd	$⊢ n \in V \to ⦋ n / k ⦌ (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = ({\sum_{R}}_{l = 0}^{n}, (A (l) \underset{˙}{} C (n - l))) \underset{˙}{\cdot} (n \underset{˙}{\times} X)$
32	14 31	ax-mp	$⊢ ⦋ n / k ⦌ (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = ({\sum_{R}}_{l = 0}^{n}, (A (l) \underset{˙}{} C (n - l))) \underset{˙}{\cdot} (n \underset{˙}{\times} X)$
33		oveq1	$⊢ {\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))) \underset{˙}{\cdot} (n \underset{˙}{\times} X) = 0_{R} \underset{˙}{\cdot} (n \underset{˙}{\times} X)$
34	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
35	34	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to R = Scalar (P)$
36	35	ad2antrr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to R = Scalar (P)$
37	36	fveq2d	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to 0_{R} = 0_{Scalar (P)}$
38	37	oveq1d	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to 0_{R} \underset{˙}{\cdot} (n \underset{˙}{\times} X) = 0_{Scalar (P)} \underset{˙}{\cdot} (n \underset{˙}{\times} X)$
39	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
40	39	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to P \in LMod$
41	40	ad2antrr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to P \in LMod$
42	9 2	mgpbas	$⊢ B = {Base}_{M}$
43	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
44	9	ringmgp	$⊢ P \in Ring \to M \in Mnd$
45	43 44	syl	$⊢ R \in Ring \to M \in Mnd$
46	45	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to M \in Mnd$
47	46	ad2antrr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to M \in Mnd$
48		simpr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
49	5 1 2	vr1cl	$⊢ R \in Ring \to X \in B$
50	49	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to X \in B$
51	50	ad2antrr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to X \in B$
52	42 10 47 48 51	mulgnn0cld	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in B$
53		eqid	$⊢ Scalar (P) = Scalar (P)$
54		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
55		eqid	$⊢ 0_{P} = 0_{P}$
56	2 53 7 54 55	lmod0vs	$⊢ (P \in LMod \land n \underset{˙}{\times} X \in B) \to 0_{Scalar (P)} \underset{˙}{\cdot} (n \underset{˙}{\times} X) = 0_{P}$
57	41 52 56	syl2anc	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to 0_{Scalar (P)} \underset{˙}{\cdot} (n \underset{˙}{\times} X) = 0_{P}$
58	38 57	eqtrd	$⊢ (((R \in Ring \land K \in B \land L \in B) \land s \in ℕ_{0}) \land n \in ℕ_{0}) \to 0_{R} \underset{˙}{\cdot} (n \underset{˙}{\times} X) = 0_{P}$
59	33 58	sylan9eqr	$⊢ ((((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))) \underset{˙}{\cdot} (n \underset{˙}{\times} X) = 0_{P}$
60	32 59	eqtrid	$⊢ ((((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))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = 0_{P}$
61	60	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))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = 0_{P})$
62	61	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))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = 0_{P}))$
63	62	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))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = 0_{P}))$
64	63	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))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = 0_{P}))$
65	13 64	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))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = 0_{P})$
66	11 12 65	mptnn0fsupp	$⊢ (R \in Ring \land K \in B \land L \in B) \to {finSupp}_{0_{P}} ((k \in ℕ_{0} ⟼ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)))$

Metamath Proof Explorer

Theorem ply1mulgsumlem4

Proof