chfacfpmmulgsum2

Description: Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019)

	Ref	Expression
Hypotheses	cayhamlem1.a	$⊢ A = N Mat R$
	cayhamlem1.b	$⊢ B = {Base}_{A}$
	cayhamlem1.p	$⊢ P = {Poly}_{1} (R)$
	cayhamlem1.y	$⊢ Y = N Mat P$
	cayhamlem1.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	cayhamlem1.s	$⊢ \underset{˙}{-} = -_{Y}$
	cayhamlem1.0	$⊢ \underset{˙}{0} = 0_{Y}$
	cayhamlem1.t	$⊢ T = N matToPolyMat R$
	cayhamlem1.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
	cayhamlem1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Y}}$
	chfacfpmmulgsum.p	$⊢ \underset{˙}{+} = +_{Y}$
Assertion	chfacfpmmulgsum2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} G (i)) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$

Proof

Step	Hyp	Ref	Expression
1		cayhamlem1.a	$⊢ A = N Mat R$
2		cayhamlem1.b	$⊢ B = {Base}_{A}$
3		cayhamlem1.p	$⊢ P = {Poly}_{1} (R)$
4		cayhamlem1.y	$⊢ Y = N Mat P$
5		cayhamlem1.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
6		cayhamlem1.s	$⊢ \underset{˙}{-} = -_{Y}$
7		cayhamlem1.0	$⊢ \underset{˙}{0} = 0_{Y}$
8		cayhamlem1.t	$⊢ T = N matToPolyMat R$
9		cayhamlem1.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
10		cayhamlem1.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Y}}$
11		chfacfpmmulgsum.p	$⊢ \underset{˙}{+} = +_{Y}$
12	1 2 3 4 5 6 7 8 9 10 11	chfacfpmmulgsum	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} G (i)) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
13		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
14		crngring	$⊢ R \in CRing \to R \in Ring$
15	14	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
16	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
17	15 16	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
18	17	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
19	18	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to Y \in Ring$
20		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
21	20	ringmgp	$⊢ Y \in Ring \to {mulGrp}_{Y} \in Mnd$
22		mndmgm	$⊢ {mulGrp}_{Y} \in Mnd \to {mulGrp}_{Y} \in Mgm$
23	21 22	syl	$⊢ Y \in Ring \to {mulGrp}_{Y} \in Mgm$
24	18 23	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{Y} \in Mgm$
25	24	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to {mulGrp}_{Y} \in Mgm$
26		elfznn	$⊢ i \in (1 \dots s) \to i \in ℕ$
27	26	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to i \in ℕ$
28	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
29	14 28	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
30	29	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to T (M) \in {Base}_{Y}$
31	20 13	mgpbas	$⊢ {Base}_{Y} = {Base}_{{mulGrp}_{Y}}$
32	31 10	mulgnncl	$⊢ ({mulGrp}_{Y} \in Mgm \land i \in ℕ \land T (M) \in {Base}_{Y}) \to i \underset{˙}{\times} T (M) \in {Base}_{Y}$
33	25 27 30 32	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to i \underset{˙}{\times} T (M) \in {Base}_{Y}$
34	15	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
35	34	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (N \in Fin \land R \in Ring)$
36		elmapi	$⊢ b \in (B^{(0 \dots s)}) \to b : (0 \dots s) ⟶ B$
37	36	adantl	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b : (0 \dots s) ⟶ B$
38	37	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to b : (0 \dots s) ⟶ B$
39	38	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to b : (0 \dots s) ⟶ B$
40		1nn0	$⊢ 1 \in ℕ_{0}$
41	40	a1i	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to 1 \in ℕ_{0}$
42		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
43	42	adantr	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to s \in ℕ_{0}$
44		nnge1	$⊢ s \in ℕ \to 1 \leq s$
45	44	adantr	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to 1 \leq s$
46		elfz2nn0	$⊢ 1 \in (0 \dots s) \leftrightarrow (1 \in ℕ_{0} \land s \in ℕ_{0} \land 1 \leq s)$
47	41 43 45 46	syl3anbrc	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to 1 \in (0 \dots s)$
48		simpr	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i \in (1 \dots s)$
49		fz0fzdiffz0	$⊢ (1 \in (0 \dots s) \land i \in (1 \dots s)) \to i - 1 \in (0 \dots s)$
50	47 48 49	syl2anc	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i - 1 \in (0 \dots s)$
51	50	ex	$⊢ s \in ℕ \to (i \in (1 \dots s) \to i - 1 \in (0 \dots s))$
52	51	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (i \in (1 \dots s) \to i - 1 \in (0 \dots s))$
53	52	imp	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to i - 1 \in (0 \dots s)$
54	39 53	ffvelcdmd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to b (i - 1) \in B$
55		df-3an	$⊢ (N \in Fin \land R \in Ring \land b (i - 1) \in B) \leftrightarrow ((N \in Fin \land R \in Ring) \land b (i - 1) \in B)$
56	35 54 55	sylanbrc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (N \in Fin \land R \in Ring \land b (i - 1) \in B)$
57	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (i - 1) \in B) \to T (b (i - 1)) \in {Base}_{Y}$
58	56 57	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to T (b (i - 1)) \in {Base}_{Y}$
59	34 16	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
60	59	ad2antrr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to Y \in Ring$
61		simpl1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to N \in Fin$
62	14	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
63	62	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to R \in Ring$
64	42	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s \in ℕ_{0}$
65	61 63 64	3jca	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (N \in Fin \land R \in Ring \land s \in ℕ_{0})$
66	65	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (N \in Fin \land R \in Ring \land s \in ℕ_{0})$
67		simpr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b \in (B^{(0 \dots s)})$
68	67	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to b \in (B^{(0 \dots s)})$
69		fz1ssfz0	$⊢ (1 \dots s) \subseteq (0 \dots s)$
70	69	sseli	$⊢ i \in (1 \dots s) \to i \in (0 \dots s)$
71	68 70	anim12i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (b \in (B^{(0 \dots s)}) \land i \in (0 \dots s))$
72	1 2 3 4 8	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}$
73	66 71 72	syl2anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to T (b (i)) \in {Base}_{Y}$
74	13 5	ringcl	$⊢ (Y \in Ring \land T (M) \in {Base}_{Y} \land T (b (i)) \in {Base}_{Y}) \to T (M) \underset{˙}{\times} T (b (i)) \in {Base}_{Y}$
75	60 30 73 74	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to T (M) \underset{˙}{\times} T (b (i)) \in {Base}_{Y}$
76	13 5 6 19 33 58 75	ringsubdi	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))) = ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (M) \underset{˙}{\times} T (b (i))))$
77	13 5	ringass	$⊢ (Y \in Ring \land (i \underset{˙}{\times} T (M) \in {Base}_{Y} \land T (M) \in {Base}_{Y} \land T (b (i)) \in {Base}_{Y})) \to ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)) = (i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (M) \underset{˙}{\times} T (b (i)))$
78	60 33 30 73 77	syl13anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)) = (i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (M) \underset{˙}{\times} T (b (i)))$
79	78	eqcomd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (M) \underset{˙}{\times} T (b (i))) = ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))$
80	29 31	eleqtrdi	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{{mulGrp}_{Y}}$
81	80	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (M) \in {Base}_{{mulGrp}_{Y}}$
82		eqid	$⊢ {Base}_{{mulGrp}_{Y}} = {Base}_{{mulGrp}_{Y}}$
83		eqid	$⊢ +_{{mulGrp}_{Y}} = +_{{mulGrp}_{Y}}$
84	82 10 83	mulgnnp1	$⊢ (i \in ℕ \land T (M) \in {Base}_{{mulGrp}_{Y}}) \to (i + 1) \underset{˙}{\times} T (M) = (i \underset{˙}{\times} T (M)) +_{{mulGrp}_{Y}} T (M)$
85	26 81 84	syl2anr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i + 1) \underset{˙}{\times} T (M) = (i \underset{˙}{\times} T (M)) +_{{mulGrp}_{Y}} T (M)$
86	20 5	mgpplusg	$⊢ \underset{˙}{\times} = +_{{mulGrp}_{Y}}$
87	86	eqcomi	$⊢ +_{{mulGrp}_{Y}} = \underset{˙}{\times}$
88	87	a1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to +_{{mulGrp}_{Y}} = \underset{˙}{\times}$
89	88	oveqd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i \underset{˙}{\times} T (M)) +_{{mulGrp}_{Y}} T (M) = (i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (M)$
90	85 89	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i + 1) \underset{˙}{\times} T (M) = (i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (M)$
91	90	eqcomd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (M) = (i + 1) \underset{˙}{\times} T (M)$
92	91	oveq1d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)) = ((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))$
93	79 92	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (M) \underset{˙}{\times} T (b (i))) = ((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))$
94	93	oveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (M) \underset{˙}{\times} T (b (i)))) = ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)))$
95	76 94	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))) = ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)))$
96	95	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i))))) = (i \in (1 \dots s) ⟼ ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))))$
97	96	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 1}^{s} ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i))))) = {\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))))$
98	97	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
99	12 98	eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} G (i)) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$

Metamath Proof Explorer

Theorem chfacfpmmulgsum2

Proof