ply1mulgsum

Description: The product of two polynomials expressed as group sum of scaled monomials. (Contributed by AV, 20-Oct-2019)

	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	ply1mulgsum	$⊢ (R \in Ring \land K \in B \land L \in B) \to K \underset{˙}{\times} L = \underset{k \in ℕ_{0}}{\sum_{P}} (({\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	1 6 8 2	coe1mul	$⊢ (R \in Ring \land K \in B \land L \in B) \to {coe}_{1} (K \underset{˙}{\times} L) = (m \in ℕ_{0} ⟼ {\sum_{R}}_{i = 0}^{m} ({coe}_{1} (K) (i) \underset{˙}{*} {coe}_{1} (L) (m - i)))$
12	11	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to {coe}_{1} (K \underset{˙}{\times} L) = (m \in ℕ_{0} ⟼ {\sum_{R}}_{i = 0}^{m} ({coe}_{1} (K) (i) \underset{˙}{*} {coe}_{1} (L) (m - i)))$
13	12	fveq1d	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to {coe}_{1} (K \underset{˙}{\times} L) (n) = (m \in ℕ_{0} ⟼ {\sum_{R}}_{i = 0}^{m} ({coe}_{1} (K) (i) \underset{˙}{*} {coe}_{1} (L) (m - i))) (n)$
14		eqidd	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to (m \in ℕ_{0} ⟼ {\sum_{R}}_{i = 0}^{m} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (m - i))) = (m \in ℕ_{0} ⟼ {\sum_{R}}_{i = 0}^{m} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (m - i)))$
15		oveq2	$⊢ m = n \to (0 \dots m) = (0 \dots n)$
16		fvoveq1	$⊢ m = n \to {coe}_{1} (L) (m - i) = {coe}_{1} (L) (n - i)$
17	16	oveq2d	$⊢ m = n \to {coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (m - i) = {coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i)$
18	15 17	mpteq12dv	$⊢ m = n \to (i \in (0 \dots m) ⟼ {coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (m - i)) = (i \in (0 \dots n) ⟼ {coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i))$
19	18	oveq2d	$⊢ m = n \to {\sum_{R}}_{i = 0}^{m} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (m - i)) = {\sum_{R}}_{i = 0}^{n} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i))$
20	19	adantl	$⊢ (((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land m = n) \to {\sum_{R}}_{i = 0}^{m} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (m - i)) = {\sum_{R}}_{i = 0}^{n} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i))$
21		simpr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
22		ovexd	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to {\sum_{R}}_{i = 0}^{n} ({coe}_{1} (K) (i) \underset{˙}{*} {coe}_{1} (L) (n - i)) \in V$
23	14 20 21 22	fvmptd	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to (m \in ℕ_{0} ⟼ {\sum_{R}}_{i = 0}^{m} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (m - i))) (n) = {\sum_{R}}_{i = 0}^{n} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i))$
24	9	fveq2i	$⊢ \cdot_{M} = \cdot_{{mulGrp}_{P}}$
25	10 24	eqtri	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
26		simp1	$⊢ (R \in Ring \land K \in B \land L \in B) \to R \in Ring$
27	26	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to R \in Ring$
28		eqid	$⊢ {Base}_{R} = {Base}_{R}$
29		eqid	$⊢ 0_{R} = 0_{R}$
30		ringcmn	$⊢ R \in Ring \to R \in CMnd$
31	30	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to R \in CMnd$
32	31	ad2antrr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to R \in CMnd$
33		fzfid	$⊢ (((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to (0 \dots k) \in Fin$
34		simpll1	$⊢ (((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to R \in Ring$
35	34	adantr	$⊢ ((((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to R \in Ring$
36		simp2	$⊢ (R \in Ring \land K \in B \land L \in B) \to K \in B$
37	36	ad2antrr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to K \in B$
38		elfznn0	$⊢ l \in (0 \dots k) \to l \in ℕ_{0}$
39	3 2 1 28	coe1fvalcl	$⊢ (K \in B \land l \in ℕ_{0}) \to A (l) \in {Base}_{R}$
40	37 38 39	syl2an	$⊢ ((((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to A (l) \in {Base}_{R}$
41		simp3	$⊢ (R \in Ring \land K \in B \land L \in B) \to L \in B$
42	41	ad2antrr	$⊢ (((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to L \in B$
43		fznn0sub	$⊢ l \in (0 \dots k) \to k - l \in ℕ_{0}$
44	4 2 1 28	coe1fvalcl	$⊢ (L \in B \land k - l \in ℕ_{0}) \to C (k - l) \in {Base}_{R}$
45	42 43 44	syl2an	$⊢ ((((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to C (k - l) \in {Base}_{R}$
46	28 8	ringcl	$⊢ (R \in Ring \land A (l) \in {Base}_{R} \land C (k - l) \in {Base}_{R}) \to A (l) \underset{˙}{*} C (k - l) \in {Base}_{R}$
47	35 40 45 46	syl3anc	$⊢ ((((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to A (l) \underset{˙}{*} C (k - l) \in {Base}_{R}$
48	47	ralrimiva	$⊢ (((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to \forall l \in (0 \dots k) A (l) \underset{˙}{*} C (k - l) \in {Base}_{R}$
49	28 32 33 48	gsummptcl	$⊢ (((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \land k \in ℕ_{0}) \to {\sum_{R}}_{l = 0}^{k} (A (l) \underset{˙}{*} C (k - l)) \in {Base}_{R}$
50	49	ralrimiva	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to \forall k \in ℕ_{0} {\sum_{R}}_{l = 0}^{k} (A (l) \underset{˙}{*} C (k - l)) \in {Base}_{R}$
51	1 2 3 4 5 6 7 8 9 10	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))))$
52	51	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to {finSupp}_{0_{R}} ((k \in ℕ_{0} ⟼ {\sum_{R}}_{l = 0}^{k} (A (l) \underset{˙}{*} C (k - l))))$
53	1 2 5 25 27 28 7 29 50 52 21	gsummoncoe1	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X))) (n) = ⦋ n / k ⦌ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l)))$
54		vex	$⊢ n \in V$
55		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))$
56		id	$⊢ n \in V \to n \in V$
57		oveq2	$⊢ k = n \to (0 \dots k) = (0 \dots n)$
58		fvoveq1	$⊢ k = n \to C (k - l) = C (n - l)$
59	58	oveq2d	$⊢ k = n \to A (l) \underset{˙}{} C (k - l) = A (l) \underset{˙}{} C (n - l)$
60	57 59	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))$
61	60	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))$
62	56 61	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))$
63	62	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))$
64	55 63	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))$
65	54 64	mp1i	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \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))$
66		fveq2	$⊢ l = i \to A (l) = A (i)$
67	3	fveq1i	$⊢ A (i) = {coe}_{1} (K) (i)$
68	66 67	eqtrdi	$⊢ l = i \to A (l) = {coe}_{1} (K) (i)$
69		oveq2	$⊢ l = i \to n - l = n - i$
70	69	fveq2d	$⊢ l = i \to C (n - l) = C (n - i)$
71	4	fveq1i	$⊢ C (n - i) = {coe}_{1} (L) (n - i)$
72	70 71	eqtrdi	$⊢ l = i \to C (n - l) = {coe}_{1} (L) (n - i)$
73	68 72	oveq12d	$⊢ l = i \to A (l) \underset{˙}{} C (n - l) = {coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i)$
74	73	cbvmptv	$⊢ (l \in (0 \dots n) ⟼ A (l) \underset{˙}{} C (n - l)) = (i \in (0 \dots n) ⟼ {coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i))$
75	74	a1i	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to (l \in (0 \dots n) ⟼ A (l) \underset{˙}{} C (n - l)) = (i \in (0 \dots n) ⟼ {coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i))$
76	75	oveq2d	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to {\sum_{R}}_{l = 0}^{n} (A (l) \underset{˙}{} C (n - l)) = {\sum_{R}}_{i = 0}^{n} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i))$
77	53 65 76	3eqtrrd	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to {\sum_{R}}_{i = 0}^{n} ({coe}_{1} (K) (i) \underset{˙}{} {coe}_{1} (L) (n - i)) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X))) (n)$
78	13 23 77	3eqtrd	$⊢ ((R \in Ring \land K \in B \land L \in B) \land n \in ℕ_{0}) \to {coe}_{1} (K \underset{˙}{\times} L) (n) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X))) (n)$
79	78	ralrimiva	$⊢ (R \in Ring \land K \in B \land L \in B) \to \forall n \in ℕ_{0} {coe}_{1} (K \underset{˙}{\times} L) (n) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X))) (n)$
80	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
81	2 6	ringcl	$⊢ (P \in Ring \land K \in B \land L \in B) \to K \underset{˙}{\times} L \in B$
82	80 81	syl3an1	$⊢ (R \in Ring \land K \in B \land L \in B) \to K \underset{˙}{\times} L \in B$
83		eqid	$⊢ 0_{P} = 0_{P}$
84		ringcmn	$⊢ P \in Ring \to P \in CMnd$
85	80 84	syl	$⊢ R \in Ring \to P \in CMnd$
86	85	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to P \in CMnd$
87		nn0ex	$⊢ ℕ_{0} \in V$
88	87	a1i	$⊢ (R \in Ring \land K \in B \land L \in B) \to ℕ_{0} \in V$
89	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
90	89	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to P \in LMod$
91	90	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to P \in LMod$
92	31	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to R \in CMnd$
93		fzfid	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to (0 \dots k) \in Fin$
94		simpll1	$⊢ (((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to R \in Ring$
95	36	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to K \in B$
96	95 38 39	syl2an	$⊢ (((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to A (l) \in {Base}_{R}$
97	41	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to L \in B$
98	97 43 44	syl2an	$⊢ (((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to C (k - l) \in {Base}_{R}$
99	94 96 98 46	syl3anc	$⊢ (((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \land l \in (0 \dots k)) \to A (l) \underset{˙}{*} C (k - l) \in {Base}_{R}$
100	99	ralrimiva	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to \forall l \in (0 \dots k) A (l) \underset{˙}{*} C (k - l) \in {Base}_{R}$
101	28 92 93 100	gsummptcl	$⊢ ((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 {Base}_{R}$
102	26	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to R \in Ring$
103	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
104	102 103	syl	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to R = Scalar (P)$
105	104	fveq2d	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to {Base}_{R} = {Base}_{Scalar (P)}$
106	101 105	eleqtrd	$⊢ ((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 {Base}_{Scalar (P)}$
107	9 2	mgpbas	$⊢ B = {Base}_{M}$
108	9	ringmgp	$⊢ P \in Ring \to M \in Mnd$
109	80 108	syl	$⊢ R \in Ring \to M \in Mnd$
110	109	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to M \in Mnd$
111	110	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to M \in Mnd$
112		simpr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
113	5 1 2	vr1cl	$⊢ R \in Ring \to X \in B$
114	113	3ad2ant1	$⊢ (R \in Ring \land K \in B \land L \in B) \to X \in B$
115	114	adantr	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to X \in B$
116	107 10 111 112 115	mulgnn0cld	$⊢ ((R \in Ring \land K \in B \land L \in B) \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in B$
117		eqid	$⊢ Scalar (P) = Scalar (P)$
118		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
119	2 117 7 118	lmodvscl	$⊢ (P \in LMod \land {\sum_{R}}_{l = 0}^{k} (A (l) \underset{˙}{} C (k - l)) \in {Base}_{Scalar (P)} \land k \underset{˙}{\times} X \in B) \to ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X) \in B$
120	91 106 116 119	syl3anc	$⊢ ((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 B$
121	120	fmpttd	$⊢ (R \in Ring \land K \in B \land L \in B) \to (k \in ℕ_{0} ⟼ ({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) : ℕ_{0} ⟶ B$
122	1 2 3 4 5 6 7 8 9 10	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)))$
123	2 83 86 88 121 122	gsumcl	$⊢ (R \in Ring \land K \in B \land L \in B) \to \underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \in B$
124		eqid	$⊢ {coe}_{1} (K \underset{˙}{\times} L) = {coe}_{1} (K \underset{˙}{\times} L)$
125		eqid	$⊢ {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X))) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)))$
126	1 2 124 125	ply1coe1eq	$⊢ (R \in Ring \land K \underset{˙}{\times} L \in B \land \underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) \in B) \to (\forall n \in ℕ_{0} {coe}_{1} (K \underset{˙}{\times} L) (n) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X))) (n) \leftrightarrow K \underset{˙}{\times} L = \underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)))$
127	26 82 123 126	syl3anc	$⊢ (R \in Ring \land K \in B \land L \in B) \to (\forall n \in ℕ_{0} {coe}_{1} (K \underset{˙}{\times} L) (n) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X))) (n) \leftrightarrow K \underset{˙}{\times} L = \underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X)))$
128	79 127	mpbid	$⊢ (R \in Ring \land K \in B \land L \in B) \to K \underset{˙}{\times} L = \underset{k \in ℕ_{0}}{\sum_{P}} (({\sum_{R}}_{l = 0}^{k}, (A (l) \underset{˙}{*} C (k - l))) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$

Metamath Proof Explorer

Theorem ply1mulgsum

Proof