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	mulgnn0cl	$⊢ ({mulGrp}_{P} \in Mnd \land i \in ℕ_{0} \land X \in {Base}_{P}) \to i \underset{˙}{\times} X \in {Base}_{P}$
72	18 20 27 71	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 \in {Base}_{P}$
73	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}$
74	72 73	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)}$
75	46 48	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
76	75	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
77	58 10	ringidcl	$⊢ Y \in Ring \to \underset{˙}{1} \in {Base}_{Y}$
78	76 77	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{˙}{1} \in {Base}_{Y}$
79	78	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}$
80		eqid	$⊢ Scalar (Y) = Scalar (Y)$
81		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
82		eqid	$⊢ \cdot_{Scalar (Y)} = \cdot_{Scalar (Y)}$
83	58 80 81 82 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)))$
84	66 70 74 79 57 83	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)))$
85	84	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)))$
86	62 85	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)))$
87	86	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))))$
88	87	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))))$
89		eqid	$⊢ 0_{Y} = 0_{Y}$
90		eqid	$⊢ +_{Y} = +_{Y}$
91	76	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$
92		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$
93	4	matlmod	$⊢ (N \in Fin \land P \in Ring) \to Y \in LMod$
94	46 93	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in LMod$
95	94	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in LMod$
96	11	adantl	$⊢ (N \in Fin \land R \in CRing) \to R \in Ring$
97	96 25	syl	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{P}$
98	34 36	syl	$⊢ (N \in Fin \land R \in CRing) \to P = Scalar (Y)$
99	98	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to Scalar (Y) = P$
100	99	fveq2d	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{Scalar (Y)} = {Base}_{P}$
101	97 100	eleqtrrd	$⊢ (N \in Fin \land R \in CRing) \to X \in {Base}_{Scalar (Y)}$
102	101	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{Scalar (Y)}$
103	49 77	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{˙}{1} \in {Base}_{Y}$
104	58 80 8 81	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}$
105	95 102 103 104	syl3anc	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \underset{˙}{\cdot} \underset{˙}{1} \in {Base}_{Y}$
106	105	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}$
107	95	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$
108	36	eqcomd	$⊢ (N \in Fin \land P \in CRing) \to Scalar (Y) = P$
109	108	fveq2d	$⊢ (N \in Fin \land P \in CRing) \to {Base}_{Scalar (Y)} = {Base}_{P}$
110	35 109	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
111	110	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})$
112	111	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})$
113	72 112	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)}$
114	58 80 8 81	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}$
115	107 113 57 114	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}$
116		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$
117	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$
118		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}$
119		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)))$
120		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$
121		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$
122		fvexd	$⊢ ((N \in Fin \land R \in Ring \land s \in ℕ_{0}) \land b \in (B^{(0 \dots s)})) \to 0_{Y} \in V$
123	119 120 121 122	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))))$
124	116 117 118 54 123	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))))$
125	58 89 90 9 91 92 106 115 124	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))))$
126	88 125	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