cpmadugsumlemF

	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}$
	cpmadugsum.g	$⊢ \underset{˙}{+} = +_{Y}$
	cpmadugsum.s	$⊢ \underset{˙}{-} = -_{Y}$
Assertion	cpmadugsumlemF	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \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))))) \underset{˙}{-} (T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$

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		cpmadugsum.g	$⊢ \underset{˙}{+} = +_{Y}$
12		cpmadugsum.s	$⊢ \underset{˙}{-} = -_{Y}$
13		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
14	1 2 3 4 5 6 7 8 9 10	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)))$
15	13 14	sylanr1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \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)))$
16	1 2 3 4 5 6 7 8 9 10	cpmadugsumlemC	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ_{0} \land b \in (B^{(0 \dots s)}))) \to T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = {\sum_{Y}}_{i = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))$
17	13 16	sylanr1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = {\sum_{Y}}_{i = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))$
18	15 17	oveq12d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \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))))) \underset{˙}{-} (T (M) \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)))) \underset{˙}{-} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))$
19		nncn	$⊢ s \in ℕ \to s \in ℂ$
20		npcan1	$⊢ s \in ℂ \to s - 1 + 1 = s$
21	20	eqcomd	$⊢ s \in ℂ \to s = s - 1 + 1$
22	19 21	syl	$⊢ s \in ℕ \to s = s - 1 + 1$
23	22	oveq2d	$⊢ s \in ℕ \to (0 \dots s) = (0 \dots s - 1 + 1)$
24	23	mpteq1d	$⊢ s \in ℕ \to (i \in (0 \dots s) ⟼ ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = (i \in (0 \dots s - 1 + 1) ⟼ ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
25	24	oveq2d	$⊢ s \in ℕ \to {\sum_{Y}}_{i = 0}^{s} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = {\sum_{Y}}_{i = 0}^{s - 1 + 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
26	25	ad2antrl	$⊢ ((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 = 0}^{s} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = {\sum_{Y}}_{i = 0}^{s - 1 + 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))$
27		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
28		crngring	$⊢ R \in CRing \to R \in Ring$
29	28	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
30	29	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
31	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
32	30 31	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
33		ringcmn	$⊢ Y \in Ring \to Y \in CMnd$
34	32 33	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in CMnd$
35	34	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in CMnd$
36		nnm1nn0	$⊢ s \in ℕ \to s - 1 \in ℕ_{0}$
37	36	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s - 1 \in ℕ_{0}$
38		simpll1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s - 1 + 1)) \to N \in Fin$
39	28	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
40	39	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$
41	40	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 (0 \dots s - 1 + 1)) \to R \in Ring$
42		elmapi	$⊢ b \in (B^{(0 \dots s)}) \to b : (0 \dots s) ⟶ B$
43	23	feq2d	$⊢ s \in ℕ \to (b : (0 \dots s) ⟶ B \leftrightarrow b : (0 \dots s - 1 + 1) ⟶ B)$
44	42 43	syl5ibcom	$⊢ b \in (B^{(0 \dots s)}) \to (s \in ℕ \to b : (0 \dots s - 1 + 1) ⟶ B)$
45	44	impcom	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b : (0 \dots s - 1 + 1) ⟶ B$
46	45	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 - 1 + 1) ⟶ B$
47	46	ffvelrnda	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s - 1 + 1)) \to b (i) \in B$
48		elfznn0	$⊢ i \in (0 \dots s - 1 + 1) \to i \in ℕ_{0}$
49	48	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 (0 \dots s - 1 + 1)) \to i \in ℕ_{0}$
50		1nn0	$⊢ 1 \in ℕ_{0}$
51	50	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 (0 \dots s - 1 + 1)) \to 1 \in ℕ_{0}$
52	49 51	nn0addcld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s - 1 + 1)) \to i + 1 \in ℕ_{0}$
53	1 2 5 3 4 27 8 7 6	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (b (i) \in B \land i + 1 \in ℕ_{0})) \to ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
54	38 41 47 52 53	syl22anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s - 1 + 1)) \to ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
55	27 11 35 37 54	gsummptfzsplit	$⊢ ((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 = 0}^{s - 1 + 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (\underset{i \in \{s - 1 + 1\}}{\sum_{Y}}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
56		ringmnd	$⊢ Y \in Ring \to Y \in Mnd$
57	32 56	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Mnd$
58	57	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in Mnd$
59		ovexd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s - 1 + 1 \in V$
60		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$
61		nn0fz0	$⊢ s \in ℕ_{0} \leftrightarrow s \in (0 \dots s)$
62	13 61	sylib	$⊢ s \in ℕ \to s \in (0 \dots s)$
63		ffvelrn	$⊢ (b : (0 \dots s) ⟶ B \land s \in (0 \dots s)) \to b (s) \in B$
64	42 62 63	syl2anr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b (s) \in B$
65	13	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s \in ℕ_{0}$
66	50	a1i	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to 1 \in ℕ_{0}$
67	65 66	nn0addcld	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to s + 1 \in ℕ_{0}$
68	64 67	jca	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to (b (s) \in B \land s + 1 \in ℕ_{0})$
69	68	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (b (s) \in B \land s + 1 \in ℕ_{0})$
70	1 2 5 3 4 27 8 7 6	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (b (s) \in B \land s + 1 \in ℕ_{0})) \to ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)) \in {Base}_{Y}$
71	60 40 69 70	syl21anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)) \in {Base}_{Y}$
72		oveq1	$⊢ i = s - 1 + 1 \to i + 1 = (s - 1) + 1 + 1$
73	72	oveq1d	$⊢ i = s - 1 + 1 \to (i + 1) \underset{˙}{\times} X = ((s - 1) + 1 + 1) \underset{˙}{\times} X$
74		2fveq3	$⊢ i = s - 1 + 1 \to T (b (i)) = T (b (s - 1 + 1))$
75	73 74	oveq12d	$⊢ i = s - 1 + 1 \to ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) = (((s - 1) + 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s - 1 + 1))$
76	19 20	syl	$⊢ s \in ℕ \to s - 1 + 1 = s$
77	76	oveq1d	$⊢ s \in ℕ \to (s - 1) + 1 + 1 = s + 1$
78	77	oveq1d	$⊢ s \in ℕ \to ((s - 1) + 1 + 1) \underset{˙}{\times} X = (s + 1) \underset{˙}{\times} X$
79	76	fveq2d	$⊢ s \in ℕ \to b (s - 1 + 1) = b (s)$
80	79	fveq2d	$⊢ s \in ℕ \to T (b (s - 1 + 1)) = T (b (s))$
81	78 80	oveq12d	$⊢ s \in ℕ \to (((s - 1) + 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s - 1 + 1)) = ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))$
82	81	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (((s - 1) + 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s - 1 + 1)) = ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))$
83	75 82	sylan9eqr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i = s - 1 + 1) \to ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) = ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))$
84	27 58 59 71 83	gsumsnd	$⊢ ((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 \{s - 1 + 1\}}{\sum_{Y}} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))$
85	84	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 = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (\underset{i \in \{s - 1 + 1\}}{\sum_{Y}}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) = ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))$
86	26 55 85	3eqtrd	$⊢ ((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 = 0}^{s} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))$
87	13	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}$
88	3 4	pmatlmod	$⊢ (N \in Fin \land R \in Ring) \to Y \in LMod$
89	29 88	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in LMod$
90	89	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in LMod$
91	90	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in LMod$
92	91	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 (0 \dots s)) \to Y \in LMod$
93	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
94	28 93	syl	$⊢ R \in CRing \to P \in Ring$
95	94	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
96		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
97	96	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
98	95 97	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
99	98	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {mulGrp}_{P} \in Mnd$
100	99	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 (0 \dots s)) \to {mulGrp}_{P} \in Mnd$
101		elfznn0	$⊢ i \in (0 \dots s) \to i \in ℕ_{0}$
102	101	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 (0 \dots s)) \to i \in ℕ_{0}$
103		eqid	$⊢ {Base}_{P} = {Base}_{P}$
104	6 3 103	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
105	28 104	syl	$⊢ R \in CRing \to X \in {Base}_{P}$
106	105	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{P}$
107	106	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to X \in {Base}_{P}$
108	107	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 (0 \dots s)) \to X \in {Base}_{P}$
109	96 103	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
110	109 7	mulgnn0cl	$⊢ ({mulGrp}_{P} \in Mnd \land i \in ℕ_{0} \land X \in {Base}_{P}) \to i \underset{˙}{\times} X \in {Base}_{P}$
111	100 102 108 110	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 (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{P}$
112	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
113	112	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
114	113	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
115	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
116	114 115	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (Y)$
117	116	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (Y) = P$
118	117	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
119	118	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})$
120	119	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \leftrightarrow i \underset{˙}{\times} X \in {Base}_{P})$
121	120	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 (0 \dots s)) \to (i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \leftrightarrow i \underset{˙}{\times} X \in {Base}_{P})$
122	111 121	mpbird	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to i \underset{˙}{\times} X \in {Base}_{Scalar (Y)}$
123	32	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in Ring$
124	123	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 (0 \dots s)) \to Y \in Ring$
125		simpll1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to N \in Fin$
126	40	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 (0 \dots s)) \to R \in Ring$
127		simpll3	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to M \in B$
128	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
129	125 126 127 128	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 (0 \dots s)) \to T (M) \in {Base}_{Y}$
130	87	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 (0 \dots s)) \to s \in ℕ_{0}$
131		simprr	$⊢ ((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)})$
132	131	anim1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \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))$
133	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}$
134	125 126 130 132 133	syl31anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s)) \to T (b (i)) \in {Base}_{Y}$
135	27 9	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}$
136	124 129 134 135	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 (0 \dots s)) \to T (M) \underset{˙}{\times} T (b (i)) \in {Base}_{Y}$
137		eqid	$⊢ Scalar (Y) = Scalar (Y)$
138		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
139	27 137 8 138	lmodvscl	$⊢ (Y \in LMod \land i \underset{˙}{\times} X \in {Base}_{Scalar (Y)} \land T (M) \underset{˙}{\times} T (b (i)) \in {Base}_{Y}) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))) \in {Base}_{Y}$
140	92 122 136 139	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 (0 \dots s)) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))) \in {Base}_{Y}$
141	27 11 35 87 140	gsummptfzsplitl	$⊢ ((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 = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (\underset{i \in \{0\}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))$
142		0nn0	$⊢ 0 \in ℕ_{0}$
143	142	a1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 0 \in ℕ_{0}$
144		eqid	$⊢ 0_{{mulGrp}_{P}} = 0_{{mulGrp}_{P}}$
145	109 144 7	mulg0	$⊢ X \in {Base}_{P} \to 0 \underset{˙}{\times} X = 0_{{mulGrp}_{P}}$
146	106 145	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0 \underset{˙}{\times} X = 0_{{mulGrp}_{P}}$
147	146	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 0 \underset{˙}{\times} X = 0_{{mulGrp}_{P}}$
148	147	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (0 \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) = 0_{{mulGrp}_{P}} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0)))$
149		eqid	$⊢ 1_{P} = 1_{P}$
150	96 149	ringidval	$⊢ 1_{P} = 0_{{mulGrp}_{P}}$
151	150	a1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1_{P} = 0_{{mulGrp}_{P}}$
152	151	eqcomd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 0_{{mulGrp}_{P}} = 1_{P}$
153	152	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 0_{{mulGrp}_{P}} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) = 1_{P} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0)))$
154	116	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to P = Scalar (Y)$
155	154	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1_{P} = 1_{Scalar (Y)}$
156	155	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1_{P} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) = 1_{Scalar (Y)} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0)))$
157	28 128	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
158	157	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}_{Y}$
159		simpl	$⊢ (b : (0 \dots s) ⟶ B \land s \in ℕ) \to b : (0 \dots s) ⟶ B$
160		elnn0uz	$⊢ s \in ℕ_{0} \leftrightarrow s \in ℤ_{\geq 0}$
161	13 160	sylib	$⊢ s \in ℕ \to s \in ℤ_{\geq 0}$
162		eluzfz1	$⊢ s \in ℤ_{\geq 0} \to 0 \in (0 \dots s)$
163	161 162	syl	$⊢ s \in ℕ \to 0 \in (0 \dots s)$
164	163	adantl	$⊢ (b : (0 \dots s) ⟶ B \land s \in ℕ) \to 0 \in (0 \dots s)$
165	159 164	ffvelrnd	$⊢ (b : (0 \dots s) ⟶ B \land s \in ℕ) \to b (0) \in B$
166	165	ex	$⊢ b : (0 \dots s) ⟶ B \to (s \in ℕ \to b (0) \in B)$
167	42 166	syl	$⊢ b \in (B^{(0 \dots s)}) \to (s \in ℕ \to b (0) \in B)$
168	167	impcom	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b (0) \in B$
169	168	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) \in B$
170	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (0) \in B) \to T (b (0)) \in {Base}_{Y}$
171	60 40 169 170	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (b (0)) \in {Base}_{Y}$
172	27 9	ringcl	$⊢ (Y \in Ring \land T (M) \in {Base}_{Y} \land T (b (0)) \in {Base}_{Y}) \to T (M) \underset{˙}{\times} T (b (0)) \in {Base}_{Y}$
173	123 158 171 172	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (M) \underset{˙}{\times} T (b (0)) \in {Base}_{Y}$
174		eqid	$⊢ 1_{Scalar (Y)} = 1_{Scalar (Y)}$
175	27 137 8 174	lmodvs1	$⊢ (Y \in LMod \land T (M) \underset{˙}{\times} T (b (0)) \in {Base}_{Y}) \to 1_{Scalar (Y)} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) = T (M) \underset{˙}{\times} T (b (0))$
176	91 173 175	syl2anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1_{Scalar (Y)} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) = T (M) \underset{˙}{\times} T (b (0))$
177	156 176	eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1_{P} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) = T (M) \underset{˙}{\times} T (b (0))$
178	148 153 177	3eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (0 \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) = T (M) \underset{˙}{\times} T (b (0))$
179	178 173	eqeltrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (0 \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) \in {Base}_{Y}$
180		oveq1	$⊢ i = 0 \to i \underset{˙}{\times} X = 0 \underset{˙}{\times} X$
181		2fveq3	$⊢ i = 0 \to T (b (i)) = T (b (0))$
182	181	oveq2d	$⊢ i = 0 \to T (M) \underset{˙}{\times} T (b (i)) = T (M) \underset{˙}{\times} T (b (0))$
183	180 182	oveq12d	$⊢ i = 0 \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))) = (0 \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0)))$
184	183	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i = 0) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))) = (0 \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0)))$
185	27 58 143 179 184	gsumsnd	$⊢ ((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} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) = (0 \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0)))$
186	109 150 7	mulg0	$⊢ X \in {Base}_{P} \to 0 \underset{˙}{\times} X = 1_{P}$
187	106 186	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0 \underset{˙}{\times} X = 1_{P}$
188	187	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 0 \underset{˙}{\times} X = 1_{P}$
189	188	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (0 \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0))) = 1_{P} \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (0)))$
190	185 189 177	3eqtrd	$⊢ ((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} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) = T (M) \underset{˙}{\times} T (b (0))$
191	190	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} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (\underset{i \in \{0\}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (T (M) \underset{˙}{\times} T (b (0)))$
192	141 191	eqtrd	$⊢ ((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 = 0}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (T (M) \underset{˙}{\times} T (b (0)))$
193	86 192	oveq12d	$⊢ ((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 = 0}^{s}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{-} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = (({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))) \underset{˙}{-} (({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (T (M) \underset{˙}{\times} T (b (0))))$
194		fzfid	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (0 \dots s - 1) \in Fin$
195		simpll1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s - 1)) \to N \in Fin$
196	40	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 (0 \dots s - 1)) \to R \in Ring$
197	42	adantl	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b : (0 \dots s) ⟶ B$
198	197	adantr	$⊢ ((s \in ℕ \land b \in (B^{(0 \dots s)})) \land i \in (0 \dots s - 1)) \to b : (0 \dots s) ⟶ B$
199		nnz	$⊢ s \in ℕ \to s \in ℤ$
200		fzoval	$⊢ s \in ℤ \to (0 ..^s) = (0 \dots s - 1)$
201	199 200	syl	$⊢ s \in ℕ \to (0 ..^s) = (0 \dots s - 1)$
202	201	eqcomd	$⊢ s \in ℕ \to (0 \dots s - 1) = (0 ..^s)$
203	202	eleq2d	$⊢ s \in ℕ \to (i \in (0 \dots s - 1) \leftrightarrow i \in (0 ..^s))$
204		elfzofz	$⊢ i \in (0 ..^s) \to i \in (0 \dots s)$
205	203 204	syl6bi	$⊢ s \in ℕ \to (i \in (0 \dots s - 1) \to i \in (0 \dots s))$
206	205	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to (i \in (0 \dots s - 1) \to i \in (0 \dots s))$
207	206	imp	$⊢ ((s \in ℕ \land b \in (B^{(0 \dots s)})) \land i \in (0 \dots s - 1)) \to i \in (0 \dots s)$
208	198 207	ffvelrnd	$⊢ ((s \in ℕ \land b \in (B^{(0 \dots s)})) \land i \in (0 \dots s - 1)) \to b (i) \in B$
209	208	adantll	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s - 1)) \to b (i) \in B$
210		elfznn0	$⊢ i \in (0 \dots s - 1) \to i \in ℕ_{0}$
211	210	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 (0 \dots s - 1)) \to i \in ℕ_{0}$
212	50	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 (0 \dots s - 1)) \to 1 \in ℕ_{0}$
213	211 212	nn0addcld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s - 1)) \to i + 1 \in ℕ_{0}$
214	195 196 209 213 53	syl22anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s - 1)) \to ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
215	214	ralrimiva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \forall i \in (0 \dots s - 1) ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) \in {Base}_{Y}$
216	27 35 194 215	gsummptcl	$⊢ ((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 = 0}^{s - 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) \in {Base}_{Y}$
217	27 11	cmncom	$⊢ (Y \in CMnd \land {\sum_{Y}}_{i = 0}^{s - 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) \in {Base}_{Y} \land ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)) \in {Base}_{Y}) \to ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
218	35 216 71 217	syl3anc	$⊢ ((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 = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))$
219	218	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 = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))) \underset{˙}{-} (({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (T (M) \underset{˙}{\times} T (b (0)))) = ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} (({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (T (M) \underset{˙}{\times} T (b (0))))$
220		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
221	32 220	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Grp$
222	221	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in Grp$
223		fzfid	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (1 \dots s) \in Fin$
224	91	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 Y \in LMod$
225	99	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 {mulGrp}_{P} \in Mnd$
226		elfznn	$⊢ i \in (1 \dots s) \to i \in ℕ$
227	226	nnnn0d	$⊢ i \in (1 \dots s) \to i \in ℕ_{0}$
228	227	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 ℕ_{0}$
229	107	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 X \in {Base}_{P}$
230	225 228 229 110	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} X \in {Base}_{P}$
231	116	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{P} = {Base}_{Scalar (Y)}$
232	231	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {Base}_{P} = {Base}_{Scalar (Y)}$
233	232	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 {Base}_{P} = {Base}_{Scalar (Y)}$
234	230 233	eleqtrd	$⊢ (((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} X \in {Base}_{Scalar (Y)}$
235	123	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 Y \in Ring$
236	158	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 T (M) \in {Base}_{Y}$
237		simpll1	$⊢ (((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$
238	40	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 R \in Ring$
239	197	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$
240	239	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$
241		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
242		fzss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 \dots s) \subseteq (0 \dots s)$
243	241 242	mp1i	$⊢ s \in ℕ \to (1 \dots s) \subseteq (0 \dots s)$
244	243	sseld	$⊢ s \in ℕ \to (i \in (1 \dots s) \to i \in (0 \dots s))$
245	244	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 \in (0 \dots s))$
246	245	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 \in (0 \dots s)$
247	240 246	ffvelrnd	$⊢ (((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) \in B$
248	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (i) \in B) \to T (b (i)) \in {Base}_{Y}$
249	237 238 247 248	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 (b (i)) \in {Base}_{Y}$
250	235 236 249 135	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}$
251	224 234 250 139	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} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))) \in {Base}_{Y}$
252	251	ralrimiva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \forall i \in (1 \dots s) (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))) \in {Base}_{Y}$
253	27 35 223 252	gsummptcl	$⊢ ((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} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) \in {Base}_{Y}$
254	27 11 12	grpaddsubass	$⊢ (Y \in Grp \land (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)) \in {Base}_{Y} \land {\sum_{Y}}_{i = 0}^{s - 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) \in {Base}_{Y} \land {\sum_{Y}}_{i = 1}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) \in {Base}_{Y})) \to ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} (({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))))$
255	222 71 216 253 254	syl13anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} (({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))))$
256		oveq1	$⊢ x = i \to x - 1 = i - 1$
257	256	oveq1d	$⊢ x = i \to x - 1 + 1 = i - 1 + 1$
258	257	oveq1d	$⊢ x = i \to (x - 1 + 1) \underset{˙}{\times} X = (i - 1 + 1) \underset{˙}{\times} X$
259	256	fveq2d	$⊢ x = i \to b (x - 1) = b (i - 1)$
260	259	fveq2d	$⊢ x = i \to T (b (x - 1)) = T (b (i - 1))$
261	258 260	oveq12d	$⊢ x = i \to ((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1)) = ((i - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))$
262	261	cbvmptv	$⊢ (x \in (1 \dots s) ⟼ ((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1))) = (i \in (1 \dots s) ⟼ ((i - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)))$
263	226	nncnd	$⊢ i \in (1 \dots s) \to i \in ℂ$
264	263	adantl	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i \in ℂ$
265		npcan1	$⊢ i \in ℂ \to i - 1 + 1 = i$
266	264 265	syl	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i - 1 + 1 = i$
267	266	oveq1d	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to (i - 1 + 1) \underset{˙}{\times} X = i \underset{˙}{\times} X$
268	267	oveq1d	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to ((i - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)) = (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))$
269	268	mpteq2dva	$⊢ s \in ℕ \to (i \in (1 \dots s) ⟼ ((i - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) = (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)))$
270	262 269	syl5eq	$⊢ s \in ℕ \to (x \in (1 \dots s) ⟼ ((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1))) = (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)))$
271	270	oveq2d	$⊢ s \in ℕ \to {\sum_{Y}}_{x = 1}^{s} (((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1))) = {\sum_{Y}}_{i = 1}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)))$
272	271	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{x = 1}^{s} (((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1))) = {\sum_{Y}}_{i = 1}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)))$
273	272	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}}_{x = 1}^{s}, (((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))$
274		eqid	$⊢ 0_{Y} = 0_{Y}$
275		1zzd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1 \in ℤ$
276		0zd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 0 \in ℤ$
277	37	nn0zd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s - 1 \in ℤ$
278		oveq1	$⊢ i = x - 1 \to i + 1 = x - 1 + 1$
279	278	oveq1d	$⊢ i = x - 1 \to (i + 1) \underset{˙}{\times} X = (x - 1 + 1) \underset{˙}{\times} X$
280		2fveq3	$⊢ i = x - 1 \to T (b (i)) = T (b (x - 1))$
281	279 280	oveq12d	$⊢ i = x - 1 \to ((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)) = ((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1))$
282	27 274 35 275 276 277 214 281	gsummptshft	$⊢ ((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 = 0}^{s - 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = {\sum_{Y}}_{x = 0 + 1}^{s - 1 + 1} (((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1)))$
283		0p1e1	$⊢ 0 + 1 = 1$
284	283	a1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 0 + 1 = 1$
285	76	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s - 1 + 1 = s$
286	284 285	oveq12d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (0 + 1 \dots s - 1 + 1) = (1 \dots s)$
287	286	mpteq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (x \in (0 + 1 \dots s - 1 + 1) ⟼ ((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1))) = (x \in (1 \dots s) ⟼ ((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1)))$
288	287	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}}_{x = 0 + 1}^{s - 1 + 1} (((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1))) = {\sum_{Y}}_{x = 1}^{s} (((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1)))$
289	282 288	eqtrd	$⊢ ((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 = 0}^{s - 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) = {\sum_{Y}}_{x = 1}^{s} (((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1)))$
290	289	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 = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = ({\sum_{Y}}_{x = 1}^{s}, (((x - 1 + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (x - 1)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))$
291		ringabl	$⊢ Y \in Ring \to Y \in Abel$
292	32 291	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Abel$
293	292	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in Abel$
294	226	adantl	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i \in ℕ$
295		nnz	$⊢ i \in ℕ \to i \in ℤ$
296		elfzm1b	$⊢ (i \in ℤ \land s \in ℤ) \to (i \in (1 \dots s) \leftrightarrow i - 1 \in (0 \dots s - 1))$
297	295 199 296	syl2an	$⊢ (i \in ℕ \land s \in ℕ) \to (i \in (1 \dots s) \leftrightarrow i - 1 \in (0 \dots s - 1))$
298	201	adantl	$⊢ (i \in ℕ \land s \in ℕ) \to (0 ..^s) = (0 \dots s - 1)$
299	298	eqcomd	$⊢ (i \in ℕ \land s \in ℕ) \to (0 \dots s - 1) = (0 ..^s)$
300	299	eleq2d	$⊢ (i \in ℕ \land s \in ℕ) \to (i - 1 \in (0 \dots s - 1) \leftrightarrow i - 1 \in (0 ..^s))$
301		elfzofz	$⊢ i - 1 \in (0 ..^s) \to i - 1 \in (0 \dots s)$
302	300 301	syl6bi	$⊢ (i \in ℕ \land s \in ℕ) \to (i - 1 \in (0 \dots s - 1) \to i - 1 \in (0 \dots s))$
303	297 302	sylbid	$⊢ (i \in ℕ \land s \in ℕ) \to (i \in (1 \dots s) \to i - 1 \in (0 \dots s))$
304	303	expimpd	$⊢ i \in ℕ \to ((s \in ℕ \land i \in (1 \dots s)) \to i - 1 \in (0 \dots s))$
305	294 304	mpcom	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i - 1 \in (0 \dots s)$
306	305	ex	$⊢ s \in ℕ \to (i \in (1 \dots s) \to i - 1 \in (0 \dots s))$
307	306	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))$
308	307	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)$
309	240 308	ffvelrnd	$⊢ (((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$
310	1 2 5 3 4 27 8 7 6	mat2pmatscmxcl	$⊢ ((N \in Fin \land R \in Ring) \land (b (i - 1) \in B \land i \in ℕ_{0})) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)) \in {Base}_{Y}$
311	237 238 309 228 310	syl22anc	$⊢ (((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} X) \underset{˙}{\cdot} T (b (i - 1)) \in {Base}_{Y}$
312		eqid	$⊢ (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) = (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)))$
313		eqid	$⊢ (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) = (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))$
314	27 12 293 223 311 251 312 313	gsummptfidmsub	$⊢ ((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} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))$
315	273 290 314	3eqtr4d	$⊢ ((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 = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = {\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))$
316	315	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} (({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))))$
317	222	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 Y \in Grp$
318	27 12	grpsubcl	$⊢ (Y \in Grp \land (i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1)) \in {Base}_{Y} \land (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))) \in {Base}_{Y}) \to ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) \in {Base}_{Y}$
319	317 311 251 318	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} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) \in {Base}_{Y}$
320	319	ralrimiva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \forall i \in (1 \dots s) ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) \in {Base}_{Y}$
321	27 35 223 320	gsummptcl	$⊢ ((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} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \in {Base}_{Y}$
322	27 11	cmncom	$⊢ (Y \in CMnd \land ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)) \in {Base}_{Y} \land {\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \in {Base}_{Y}) \to (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))$
323	35 71 321 322	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))$
324	255 316 323	3eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))$
325	324	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = (({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))$
326	27 11	mndcl	$⊢ (Y \in Mnd \land ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)) \in {Base}_{Y} \land {\sum_{Y}}_{i = 0}^{s - 1} (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))) \in {Base}_{Y}) \to (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \in {Base}_{Y}$
327	58 71 216 326	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \in {Base}_{Y}$
328	27 11 12 293 327 253 173	ablsubsub4	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} (({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (T (M) \underset{˙}{\times} T (b (0))))$
329	27 11 12	grpaddsubass	$⊢ (Y \in Grp \land ({\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \in {Base}_{Y} \land ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)) \in {Base}_{Y} \land T (M) \underset{˙}{\times} T (b (0)) \in {Base}_{Y})) \to (({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
330	222 321 71 173 329	syl13anc	$⊢ ((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} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
331	325 328 330	3eqtr3d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} ({\sum_{Y}}_{i = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) \underset{˙}{-} (({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (T (M) \underset{˙}{\times} T (b (0)))) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
332	5 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}$
333	237 238 309 332	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 (b (i - 1)) \in {Base}_{Y}$
334	27 8 137 138 12 224 234 333 250	lmodsubdi	$⊢ (((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} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))) = ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))$
335	334	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} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))) = (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i))))$
336	335	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} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))$
337	336	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} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) = {\sum_{Y}}_{i = 1}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))$
338	337	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} X) \underset{˙}{\cdot} T (b (i - 1))) \underset{˙}{-} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
339	219 331 338	3eqtrd	$⊢ ((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 = 0}^{s - 1}, (((i + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i)))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s)))) \underset{˙}{-} (({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (M) \underset{˙}{\times} T (b (i))))) \underset{˙}{+} (T (M) \underset{˙}{\times} T (b (0)))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
340	18 193 339	3eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \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))))) \underset{˙}{-} (T (M) \underset{˙}{\times} ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (i))))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))) \underset{˙}{+} ((((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$

Metamath Proof Explorer

Theorem cpmadugsumlemF

Proof