cpmadugsumlemB

	Ref	Expression
Hypotheses	cpmadugsum.a	$⊢ A = N Mat R$
	cpmadugsum.b	$⊢ B = {Base}_{A}$
	cpmadugsum.p	$⊢ P = {Poly}_{1} (R)$
	cpmadugsum.y	$⊢ Y = N Mat P$
	cpmadugsum.t	$⊢ T = N matToPolyMat R$
	cpmadugsum.x	$⊢ X = {var}_{1} (R)$
	cpmadugsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	cpmadugsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	cpmadugsum.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	cpmadugsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
Assertion	cpmadugsumlemB	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = {\sum_{Y}}_{i = 0}^{s} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$

Proof

Step	Hyp	Ref	Expression
1		cpmadugsum.a	$⊢ A = N Mat R$
2		cpmadugsum.b	$⊢ B = {Base}_{A}$
3		cpmadugsum.p	$⊢ P = {Poly}_{1} (R)$
4		cpmadugsum.y	$⊢ Y = N Mat P$
5		cpmadugsum.t	$⊢ T = N matToPolyMat R$
6		cpmadugsum.x	$⊢ X = {var}_{1} (R)$
7		cpmadugsum.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
8		cpmadugsum.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
9		cpmadugsum.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
10		cpmadugsum.1	$⊢ \underset{˙}{1} = 1_{Y}$
11		crngring	$⊢ R \in CRing \to R \in Ring$
12	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
13	11 12	syl	$⊢ R \in CRing \to P \in Ring$
14	13	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
15		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
16	15	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
17	14 16	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
18	17	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to {mulGrp}_{P} \in Mnd$
19		elfznn0	$⊢ i \in (0 \dots s) \to i \in ℕ_{0}$
20	19	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \in ℕ_{0}$
21		1nn0	$⊢ 1 \in ℕ_{0}$
22	21	a1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to 1 \in ℕ_{0}$
23	11	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
24		eqid	$⊢ {Base}_{P} = {Base}_{P}$
25	6 3 24	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
26	23 25	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{P}$
27	26	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to X \in {Base}_{P}$
28	15 24	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
29		eqid	$⊢ \cdot_{P} = \cdot_{P}$
30	15 29	mgpplusg	$⊢ \cdot_{P} = +_{{mulGrp}_{P}}$
31	28 7 30	mulgnn0dir	$⊢ ({mulGrp}_{P} \in Mnd \land (i \in ℕ_{0} \land 1 \in ℕ_{0} \land X \in {Base}_{P})) \to (i + 1) \underset{˙}{\times} X = (i \underset{˙}{\times} X) \cdot_{P} (1 \underset{˙}{\times} X)$
32	18 20 22 27 31	syl13anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (i + 1) \underset{˙}{\times} X = (i \underset{˙}{\times} X) \cdot_{P} (1 \underset{˙}{\times} X)$
33	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
34	33	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
35	34	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
36	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
37	35 36	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (Y)$
38	37	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to P = Scalar (Y)$
39	38	fveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to \cdot_{P} = \cdot_{Scalar (Y)}$
40		eqidd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X = i \underset{˙}{\times} X$
41	28 7	mulg1	$⊢ X \in {Base}_{P} \to 1 \underset{˙}{\times} X = X$
42	26 41	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 1 \underset{˙}{\times} X = X$
43	42	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to 1 \underset{˙}{\times} X = X$
44	39 40 43	oveq123d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (i \underset{˙}{\times} X) \cdot_{P} (1 \underset{˙}{\times} X) = (i \underset{˙}{\times} X) \cdot_{Scalar (Y)} X$
45	32 44	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (i + 1) \underset{˙}{\times} X = (i \underset{˙}{\times} X) \cdot_{Scalar (Y)} X$
46	13	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in Ring)$
47	46	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in Ring)$
48	4	matring	$⊢ (N \in Fin \land P \in Ring) \to Y \in Ring$
49	47 48	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
50	49	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to Y \in Ring$
51		simpll1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to N \in Fin$
52	23	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to R \in Ring$
53		simplrl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to s \in ℕ_{0}$
54		simprr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to b \in (B^{(0 \dots s)})$
55	54	anim1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (b \in (B^{(0 \dots s)}) \land i \in (0 \dots s))$
56	1 2 3 4 5	m2pmfzmap	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land (b \in (B^{(0 \dots s)}) \land i \in (0 \dots s))) \to T (b (i)) \in {Base}_{Y}$
57	51 52 53 55 56	syl31anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to T (b (i)) \in {Base}_{Y}$
58		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
59	58 9 10	ringlidm	$⊢ (Y \in Ring \land T (b (i)) \in {Base}_{Y}) \to \underset{˙}{1} \underset{˙}{\times} T (b (i)) = T (b (i))$
60	50 57 59	syl2anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to \underset{˙}{1} \underset{˙}{\times} T (b (i)) = T (b (i))$
61	60	eqcomd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to T (b (i)) = \underset{˙}{1} \underset{˙}{\times} T (b (i))$
62	45 61	oveq12d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) = ((i \underset{˙}{\times} X) \cdot_{Scalar (Y)} X) \underset{˙}{\cdot} (\underset{˙}{1} \underset{˙}{\times} T (b (i)))$
63	4	matassa	$⊢ (N \in Fin \land P \in CRing) \to Y \in AssAlg$
64	34 63	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in AssAlg$
65	64	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in AssAlg$
66	65	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to Y \in AssAlg$
67	37	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (Y) = P$
68	67	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
69	26 68	eleqtrrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{Scalar (Y)}$
70	69	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to X \in {Base}_{Scalar (Y)}$
71	28 7 18 20 27	mulgnn0cld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{P}$
72	68	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to {Base}_{Scalar (Y)} = {Base}_{P}$
73	71 72	eleqtrrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{Scalar (Y)}$
74	46 48	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
75	74	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
76	58 10	ringidcl	$⊢ Y \in Ring \to \underset{˙}{1} \in {Base}_{Y}$
77	75 76	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{˙}{1} \in {Base}_{Y}$
78	77	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to \underset{˙}{1} \in {Base}_{Y}$
79		eqid	$⊢ Scalar (Y) = Scalar (Y)$
80		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
81		eqid	$⊢ \cdot_{Scalar (Y)} = \cdot_{Scalar (Y)}$
82	58 79 80 81 8 9	assa2ass	$⊢ (Y \in AssAlg \land (X \in {Base}_{Scalar (Y)} \land i \underset{˙}{\times} X \in {Base}_{Scalar (Y)}) \land (\underset{˙}{1} \in {Base}_{Y} \land T (b (i)) \in {Base}_{Y})) \to (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = ((i \underset{˙}{\times} X) \cdot_{Scalar (Y)} X) \underset{˙}{\cdot} (\underset{˙}{1} \underset{˙}{\times} T (b (i)))$
83	66 70 73 78 57 82	syl122anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = ((i \underset{˙}{\times} X) \cdot_{Scalar (Y)} X) \underset{˙}{\cdot} (\underset{˙}{1} \underset{˙}{\times} T (b (i)))$
84	83	eqcomd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to ((i \underset{˙}{\times} X) \cdot_{Scalar (Y)} X) \underset{˙}{\cdot} (\underset{˙}{1} \underset{˙}{\times} T (b (i))) = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
85	62 84	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
86	85	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to (i \in (0 \dots s) ⟼ ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = (i \in (0 \dots s) ⟼ (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
87	86	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 0}^{s} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = {\sum_{Y}}_{i = 0}^{s} ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
88		eqid	$⊢ 0_{Y} = 0_{Y}$
89	75	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to Y \in Ring$
90		ovexd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to (0 \dots s) \in V$
91	4	matlmod	$⊢ (N \in Fin \land P \in Ring) \to Y \in LMod$
92	46 91	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in LMod$
93	92	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in LMod$
94	11	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
95	94 25	syl	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{P}$
96	34 36	syl	$⊢ (N \in Fin \land R \in CRing) \to P = Scalar (Y)$
97	96	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to Scalar (Y) = P$
98	97	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{Scalar (Y)} = {Base}_{P}$
99	95 98	eleqtrrd	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{Scalar (Y)}$
100	99	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{Scalar (Y)}$
101	49 76	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{˙}{1} \in {Base}_{Y}$
102	58 79 8 80	lmodvscl	$⊢ (Y \in LMod \land X \in {Base}_{Scalar (Y)} \land \underset{˙}{1} \in {Base}_{Y}) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
103	93 100 101 102	syl3anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
104	103	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
105	93	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to Y \in LMod$
106	36	eqcomd	$⊢ (N \in Fin \land P \in CRing) \to Scalar (Y) = P$
107	106	fveq2d	$⊢ (N \in Fin \land P \in CRing) \to {Base}_{Scalar (Y)} = {Base}_{P}$
108	35 107	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
109	108	eleq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \leftrightarrow i \underset{˙}{\times} X \in {Base}_{P})$
110	109	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \leftrightarrow i \underset{˙}{\times} X \in {Base}_{P})$
111	71 110	mpbird	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{Scalar (Y)}$
112	58 79 8 80	lmodvscl	$⊢ (Y \in LMod \land i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \land T (b (i)) \in {Base}_{Y}) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
113	105 111 57 112	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
114		simpl1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to N \in Fin$
115	23	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to R \in Ring$
116		simprl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to s \in ℕ_{0}$
117		eqid	$⊢ (i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = (i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
118		fzfid	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \to (0 \dots s) \in Fin$
119		ovexd	$⊢ (((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \land i \in (0 \dots s)) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in V$
120		fvexd	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \to 0_{Y} \in V$
121	117 118 119 120	fsuppmptdm	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \to {finSupp}_{0_{Y}} ((i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
122	114 115 116 54 121	syl31anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to {finSupp}_{0_{Y}} ((i \in (0 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
123	58 88 9 89 90 104 113 122	gsummulc2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 0}^{s} ((X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
124	87 123	eqtr2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to (X \underset{˙}{\cdot} \underset{˙}{1}) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = {\sum_{Y}}_{i = 0}^{s} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$

Metamath Proof Explorer

Theorem cpmadugsumlemB

Proof