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	ffvelcdmda	$⊢ (((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		ffvelcdm	$⊢ (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		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
94		eqid	$⊢ {Base}_{P} = {Base}_{P}$
95	93 94	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
96	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
97	28 96	syl	$⊢ R \in CRing \to P \in Ring$
98	97	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
99	93	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
100	98 99	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{P} \in Mnd$
101	100	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$
102	101	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$
103		elfznn0	$⊢ i \in (0 \dots s) \to i \in ℕ_{0}$
104	103	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}$
105	6 3 94	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
106	28 105	syl	$⊢ R \in CRing \to X \in {Base}_{P}$
107	106	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \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)}))) \to X \in {Base}_{P}$
109	108	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}$
110	95 7 102 104 109	mulgnn0cld	$⊢ (((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}$
111	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
112	111	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
113	112	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
114	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
115	113 114	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (Y)$
116	115	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (Y) = P$
117	116	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (Y)} = {Base}_{P}$
118	117	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})$
119	118	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})$
120	119	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})$
121	110 120	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)}$
122	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$
123	122	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$
124		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$
125	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$
126		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$
127	5 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
128	124 125 126 127	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}$
129	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}$
130		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)})$
131	130	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))$
132	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}$
133	124 125 129 131 132	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}$
134	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}$
135	123 128 133 134	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}$
136		eqid	$⊢ Scalar (Y) = Scalar (Y)$
137		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
138	27 136 8 137	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}$
139	92 121 135 138	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}$
140	27 11 35 87 139	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)))))$
141		0nn0	$⊢ 0 \in ℕ_{0}$
142	141	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}$
143		eqid	$⊢ 0_{{mulGrp}_{P}} = 0_{{mulGrp}_{P}}$
144	95 143 7	mulg0	$⊢ X \in {Base}_{P} \to 0 \underset{˙}{\times} X = 0_{{mulGrp}_{P}}$
145	107 144	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0 \underset{˙}{\times} X = 0_{{mulGrp}_{P}}$
146	145	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}}$
147	146	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)))$
148		eqid	$⊢ 1_{P} = 1_{P}$
149	93 148	ringidval	$⊢ 1_{P} = 0_{{mulGrp}_{P}}$
150	149	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}}$
151	150	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}$
152	151	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)))$
153	115	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)$
154	153	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)}$
155	154	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)))$
156	28 127	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
157	156	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}$
158		simpl	$⊢ (b : (0 \dots s) ⟶ B \land s \in ℕ) \to b : (0 \dots s) ⟶ B$
159		elnn0uz	$⊢ s \in ℕ_{0} \leftrightarrow s \in ℤ_{\geq 0}$
160	13 159	sylib	$⊢ s \in ℕ \to s \in ℤ_{\geq 0}$
161		eluzfz1	$⊢ s \in ℤ_{\geq 0} \to 0 \in (0 \dots s)$
162	160 161	syl	$⊢ s \in ℕ \to 0 \in (0 \dots s)$
163	162	adantl	$⊢ (b : (0 \dots s) ⟶ B \land s \in ℕ) \to 0 \in (0 \dots s)$
164	158 163	ffvelcdmd	$⊢ (b : (0 \dots s) ⟶ B \land s \in ℕ) \to b (0) \in B$
165	164	ex	$⊢ b : (0 \dots s) ⟶ B \to (s \in ℕ \to b (0) \in B)$
166	42 165	syl	$⊢ b \in (B^{(0 \dots s)}) \to (s \in ℕ \to b (0) \in B)$
167	166	impcom	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b (0) \in B$
168	167	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$
169	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}$
170	60 40 168 169	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}$
171	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}$
172	122 157 170 171	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}$
173		eqid	$⊢ 1_{Scalar (Y)} = 1_{Scalar (Y)}$
174	27 136 8 173	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))$
175	91 172 174	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))$
176	155 175	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))$
177	147 152 176	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))$
178	177 172	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}$
179		oveq1	$⊢ i = 0 \to i \underset{˙}{\times} X = 0 \underset{˙}{\times} X$
180		2fveq3	$⊢ i = 0 \to T (b (i)) = T (b (0))$
181	180	oveq2d	$⊢ i = 0 \to T (M) \underset{˙}{\times} T (b (i)) = T (M) \underset{˙}{\times} T (b (0))$
182	179 181	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)))$
183	182	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)))$
184	27 58 142 178 183	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)))$
185	95 149 7	mulg0	$⊢ X \in {Base}_{P} \to 0 \underset{˙}{\times} X = 1_{P}$
186	107 185	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0 \underset{˙}{\times} X = 1_{P}$
187	186	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}$
188	187	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)))$
189	184 188 176	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))$
190	189	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)))$
191	140 190	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)))$
192	86 191	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))))$
193		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$
194		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$
195	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$
196	42	adantl	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b : (0 \dots s) ⟶ B$
197	196	adantr	$⊢ ((s \in ℕ \land b \in (B^{(0 \dots s)})) \land i \in (0 \dots s - 1)) \to b : (0 \dots s) ⟶ B$
198		nnz	$⊢ s \in ℕ \to s \in ℤ$
199		fzoval	$⊢ s \in ℤ \to (0 ..^s) = (0 \dots s - 1)$
200	198 199	syl	$⊢ s \in ℕ \to (0 ..^s) = (0 \dots s - 1)$
201	200	eqcomd	$⊢ s \in ℕ \to (0 \dots s - 1) = (0 ..^s)$
202	201	eleq2d	$⊢ s \in ℕ \to (i \in (0 \dots s - 1) \leftrightarrow i \in (0 ..^s))$
203		elfzofz	$⊢ i \in (0 ..^s) \to i \in (0 \dots s)$
204	202 203	syl6bi	$⊢ s \in ℕ \to (i \in (0 \dots s - 1) \to i \in (0 \dots s))$
205	204	adantr	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to (i \in (0 \dots s - 1) \to i \in (0 \dots s))$
206	205	imp	$⊢ ((s \in ℕ \land b \in (B^{(0 \dots s)})) \land i \in (0 \dots s - 1)) \to i \in (0 \dots s)$
207	197 206	ffvelcdmd	$⊢ ((s \in ℕ \land b \in (B^{(0 \dots s)})) \land i \in (0 \dots s - 1)) \to b (i) \in B$
208	207	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$
209		elfznn0	$⊢ i \in (0 \dots s - 1) \to i \in ℕ_{0}$
210	209	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}$
211	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}$
212	210 211	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}$
213	194 195 208 212 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}$
214	213	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}$
215	27 35 193 214	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}$
216	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))))$
217	35 215 71 216	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))))$
218	217	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))))$
219		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
220	32 219	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Grp$
221	220	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$
222		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$
223	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$
224	101	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$
225		elfznn	$⊢ i \in (1 \dots s) \to i \in ℕ$
226	225	nnnn0d	$⊢ i \in (1 \dots s) \to i \in ℕ_{0}$
227	226	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}$
228	108	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}$
229	95 7 224 227 228	mulgnn0cld	$⊢ (((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}$
230	115	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{P} = {Base}_{Scalar (Y)}$
231	230	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)}$
232	231	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)}$
233	229 232	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)}$
234	122	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$
235	157	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}$
236		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$
237	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$
238	196	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$
239	238	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$
240		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
241		fzss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 \dots s) \subseteq (0 \dots s)$
242	240 241	mp1i	$⊢ s \in ℕ \to (1 \dots s) \subseteq (0 \dots s)$
243	242	sseld	$⊢ s \in ℕ \to (i \in (1 \dots s) \to i \in (0 \dots s))$
244	243	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))$
245	244	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)$
246	239 245	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) \in B$
247	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}$
248	236 237 246 247	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}$
249	234 235 248 134	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}$
250	223 233 249 138	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}$
251	250	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}$
252	27 35 222 251	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}$
253	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))))))$
254	221 71 215 252 253	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))))))$
255		oveq1	$⊢ x = i \to x - 1 = i - 1$
256	255	oveq1d	$⊢ x = i \to x - 1 + 1 = i - 1 + 1$
257	256	oveq1d	$⊢ x = i \to (x - 1 + 1) \underset{˙}{\times} X = (i - 1 + 1) \underset{˙}{\times} X$
258	255	fveq2d	$⊢ x = i \to b (x - 1) = b (i - 1)$
259	258	fveq2d	$⊢ x = i \to T (b (x - 1)) = T (b (i - 1))$
260	257 259	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))$
261	260	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)))$
262	225	nncnd	$⊢ i \in (1 \dots s) \to i \in ℂ$
263	262	adantl	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i \in ℂ$
264		npcan1	$⊢ i \in ℂ \to i - 1 + 1 = i$
265	263 264	syl	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i - 1 + 1 = i$
266	265	oveq1d	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to (i - 1 + 1) \underset{˙}{\times} X = i \underset{˙}{\times} X$
267	266	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))$
268	267	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)))$
269	261 268	eqtrid	$⊢ 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)))$
270	269	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)))$
271	270	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)))$
272	271	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)))))$
273		eqid	$⊢ 0_{Y} = 0_{Y}$
274		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 ℤ$
275		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 ℤ$
276	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 ℤ$
277		oveq1	$⊢ i = x - 1 \to i + 1 = x - 1 + 1$
278	277	oveq1d	$⊢ i = x - 1 \to (i + 1) \underset{˙}{\times} X = (x - 1 + 1) \underset{˙}{\times} X$
279		2fveq3	$⊢ i = x - 1 \to T (b (i)) = T (b (x - 1))$
280	278 279	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))$
281	27 273 35 274 275 276 213 280	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)))$
282		0p1e1	$⊢ 0 + 1 = 1$
283	282	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$
284	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$
285	283 284	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)$
286	285	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)))$
287	286	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)))$
288	281 287	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)))$
289	288	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)))))$
290		ringabl	$⊢ Y \in Ring \to Y \in Abel$
291	32 290	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Abel$
292	291	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$
293	225	adantl	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i \in ℕ$
294		nnz	$⊢ i \in ℕ \to i \in ℤ$
295		elfzm1b	$⊢ (i \in ℤ \land s \in ℤ) \to (i \in (1 \dots s) \leftrightarrow i - 1 \in (0 \dots s - 1))$
296	294 198 295	syl2an	$⊢ (i \in ℕ \land s \in ℕ) \to (i \in (1 \dots s) \leftrightarrow i - 1 \in (0 \dots s - 1))$
297	200	adantl	$⊢ (i \in ℕ \land s \in ℕ) \to (0 ..^s) = (0 \dots s - 1)$
298	297	eqcomd	$⊢ (i \in ℕ \land s \in ℕ) \to (0 \dots s - 1) = (0 ..^s)$
299	298	eleq2d	$⊢ (i \in ℕ \land s \in ℕ) \to (i - 1 \in (0 \dots s - 1) \leftrightarrow i - 1 \in (0 ..^s))$
300		elfzofz	$⊢ i - 1 \in (0 ..^s) \to i - 1 \in (0 \dots s)$
301	299 300	syl6bi	$⊢ (i \in ℕ \land s \in ℕ) \to (i - 1 \in (0 \dots s - 1) \to i - 1 \in (0 \dots s))$
302	296 301	sylbid	$⊢ (i \in ℕ \land s \in ℕ) \to (i \in (1 \dots s) \to i - 1 \in (0 \dots s))$
303	302	expimpd	$⊢ i \in ℕ \to ((s \in ℕ \land i \in (1 \dots s)) \to i - 1 \in (0 \dots s))$
304	293 303	mpcom	$⊢ (s \in ℕ \land i \in (1 \dots s)) \to i - 1 \in (0 \dots s)$
305	304	ex	$⊢ s \in ℕ \to (i \in (1 \dots s) \to i - 1 \in (0 \dots s))$
306	305	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))$
307	306	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)$
308	239 307	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$
309	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}$
310	236 237 308 227 309	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}$
311		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)))$
312		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))))$
313	27 12 292 222 310 250 311 312	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)))))$
314	272 289 313	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)))))$
315	314	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))))))$
316	221	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$
317	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}$
318	316 310 250 317	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}$
319	318	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}$
320	27 35 222 319	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}$
321	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)))$
322	35 71 320 321	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)))$
323	254 315 322	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)))$
324	323	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)))$
325	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}$
326	58 71 215 325	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}$
327	27 11 12 292 326 252 172	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))))$
328	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))))$
329	221 320 71 172 328	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))))$
330	324 327 329	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))))$
331	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}$
332	236 237 308 331	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}$
333	27 8 136 137 12 223 233 332 249	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))))$
334	333	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))))$
335	334	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)))))$
336	335	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)))))$
337	336	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))))$
338	218 330 337	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))))$
339	18 192 338	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