chfacfscmulgsum

Description: Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019)

	Ref	Expression
Hypotheses	chfacfisf.a	$⊢ A = N Mat R$
	chfacfisf.b	$⊢ B = {Base}_{A}$
	chfacfisf.p	$⊢ P = {Poly}_{1} (R)$
	chfacfisf.y	$⊢ Y = N Mat P$
	chfacfisf.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	chfacfisf.s	$⊢ \underset{˙}{-} = -_{Y}$
	chfacfisf.0	$⊢ \underset{˙}{0} = 0_{Y}$
	chfacfisf.t	$⊢ T = N matToPolyMat R$
	chfacfisf.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
	chfacfscmulcl.x	$⊢ X = {var}_{1} (R)$
	chfacfscmulcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	chfacfscmulcl.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	chfacfscmulgsum.p	$⊢ \underset{˙}{+} = +_{Y}$
Assertion	chfacfscmulgsum	$⊢ ((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} G (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		chfacfisf.a	$⊢ A = N Mat R$
2		chfacfisf.b	$⊢ B = {Base}_{A}$
3		chfacfisf.p	$⊢ P = {Poly}_{1} (R)$
4		chfacfisf.y	$⊢ Y = N Mat P$
5		chfacfisf.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
6		chfacfisf.s	$⊢ \underset{˙}{-} = -_{Y}$
7		chfacfisf.0	$⊢ \underset{˙}{0} = 0_{Y}$
8		chfacfisf.t	$⊢ T = N matToPolyMat R$
9		chfacfisf.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
10		chfacfscmulcl.x	$⊢ X = {var}_{1} (R)$
11		chfacfscmulcl.m	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
12		chfacfscmulcl.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
13		chfacfscmulgsum.p	$⊢ \underset{˙}{+} = +_{Y}$
14		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
15		crngring	$⊢ R \in CRing \to R \in Ring$
16	15	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
17	16	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
18	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
19	17 18	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
20		ringcmn	$⊢ Y \in Ring \to Y \in CMnd$
21	19 20	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in CMnd$
22	21	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$
23		nn0ex	$⊢ ℕ_{0} \in V$
24	23	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 V$
25		simpll	$⊢ (((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}) \to (N \in Fin \land R \in CRing \land M \in B)$
26		simplr	$⊢ (((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}) \to (s \in ℕ \land b \in (B^{(0 \dots s)}))$
27		simpr	$⊢ (((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}) \to i \in ℕ_{0}$
28	25 26 27	3jca	$⊢ (((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}) \to ((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})$
29	1 2 3 4 5 6 7 8 9 10 11 12	chfacfscmulcl	$⊢ ((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}) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) \in {Base}_{Y}$
30	28 29	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in ℕ_{0}) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) \in {Base}_{Y}$
31	1 2 3 4 5 6 7 8 9 10 11 12	chfacfscmulfsupp	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {finSupp}_{\underset{˙}{0}} ((i \in ℕ_{0} ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$
32		nn0disj	$⊢ (0 \dots s + 1) \cap ℤ_{\geq (s + 1 + 1)} = \emptyset$
33	32	a1i	$⊢ ((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) \cap ℤ_{\geq (s + 1 + 1)} = \emptyset$
34		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
35		peano2nn0	$⊢ s \in ℕ_{0} \to s + 1 \in ℕ_{0}$
36	34 35	syl	$⊢ s \in ℕ \to s + 1 \in ℕ_{0}$
37		nn0split	$⊢ s + 1 \in ℕ_{0} \to ℕ_{0} = (0 \dots s + 1) \cup ℤ_{\geq (s + 1 + 1)}$
38	36 37	syl	$⊢ s \in ℕ \to ℕ_{0} = (0 \dots s + 1) \cup ℤ_{\geq (s + 1 + 1)}$
39	38	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ℕ_{0} = (0 \dots s + 1) \cup ℤ_{\geq (s + 1 + 1)}$
40	14 7 13 22 24 30 31 33 39	gsumsplit2	$⊢ ((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} G (i)) = ({\sum_{Y}}_{i = 0}^{s + 1}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (\underset{i \in ℤ_{\geq (s + 1 + 1)}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$
41		simpll	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in ℤ_{\geq (s + 1 + 1)}) \to (N \in Fin \land R \in CRing \land M \in B)$
42		simplr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in ℤ_{\geq (s + 1 + 1)}) \to (s \in ℕ \land b \in (B^{(0 \dots s)}))$
43		nncn	$⊢ s \in ℕ \to s \in ℂ$
44		add1p1	$⊢ s \in ℂ \to s + 1 + 1 = s + 2$
45	43 44	syl	$⊢ s \in ℕ \to s + 1 + 1 = s + 2$
46	45	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 + 2$
47	46	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ℤ_{\geq (s + 1 + 1)} = ℤ_{\geq (s + 2)}$
48	47	eleq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (i \in ℤ_{\geq (s + 1 + 1)} \leftrightarrow i \in ℤ_{\geq (s + 2)})$
49	48	biimpa	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in ℤ_{\geq (s + 1 + 1)}) \to i \in ℤ_{\geq (s + 2)}$
50	1 2 3 4 5 6 7 8 9 10 11 12	chfacfscmul0	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)})) \land i \in ℤ_{\geq (s + 2)}) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) = \underset{˙}{0}$
51	41 42 49 50	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 ℤ_{\geq (s + 1 + 1)}) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) = \underset{˙}{0}$
52	51	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 ℤ_{\geq (s + 1 + 1)} ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = (i \in ℤ_{\geq (s + 1 + 1)} ⟼ \underset{˙}{0})$
53	52	oveq2d	$⊢ ((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 ℤ_{\geq (s + 1 + 1)}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = \underset{i \in ℤ_{\geq (s + 1 + 1)}}{\sum_{Y}} \underset{˙}{0}$
54	15 18	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
55		ringmnd	$⊢ Y \in Ring \to Y \in Mnd$
56	54 55	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in Mnd$
57	56	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Mnd$
58		fvex	$⊢ ℤ_{\geq (s + 1 + 1)} \in V$
59	57 58	jctir	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (Y \in Mnd \land ℤ_{\geq (s + 1 + 1)} \in V)$
60	59	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 \land ℤ_{\geq (s + 1 + 1)} \in V)$
61	7	gsumz	$⊢ (Y \in Mnd \land ℤ_{\geq (s + 1 + 1)} \in V) \to \underset{i \in ℤ_{\geq (s + 1 + 1)}}{\sum_{Y}} \underset{˙}{0} = \underset{˙}{0}$
62	60 61	syl	$⊢ ((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 ℤ_{\geq (s + 1 + 1)}}{\sum_{Y}} \underset{˙}{0} = \underset{˙}{0}$
63	53 62	eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{i \in ℤ_{\geq (s + 1 + 1)}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = \underset{˙}{0}$
64	63	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 \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (\underset{i \in ℤ_{\geq (s + 1 + 1)}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) = ({\sum_{Y}}_{i = 0}^{s + 1}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} \underset{˙}{0}$
65		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$
66		elfznn0	$⊢ i \in (0 \dots s + 1) \to i \in ℕ_{0}$
67	66 28	sylan2	$⊢ (((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 \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)})) \land i \in ℕ_{0})$
68	67 29	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (0 \dots s + 1)) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) \in {Base}_{Y}$
69	68	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 \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) \in {Base}_{Y}$
70	14 22 65 69	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 \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) \in {Base}_{Y}$
71	14 13 7	mndrid	$⊢ (Y \in Mnd \land {\sum_{Y}}_{i = 0}^{s + 1} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) \in {Base}_{Y}) \to ({\sum_{Y}}_{i = 0}^{s + 1}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} \underset{˙}{0} = {\sum_{Y}}_{i = 0}^{s + 1} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))$
72	57 70 71	syl2an2r	$⊢ ((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 \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} \underset{˙}{0} = {\sum_{Y}}_{i = 0}^{s + 1} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))$
73	64 72	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 \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (\underset{i \in ℤ_{\geq (s + 1 + 1)}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) = {\sum_{Y}}_{i = 0}^{s + 1} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))$
74	34	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}$
75	14 13 22 74 68	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} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = ({\sum_{Y}}_{i = 0}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (\underset{i \in \{s + 1\}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$
76		elfznn0	$⊢ i \in (0 \dots s) \to i \in ℕ_{0}$
77	76 30	sylan2	$⊢ (((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} G (i) \in {Base}_{Y}$
78	14 13 22 74 77	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} G (i)) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (\underset{i \in \{0\}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)))$
79	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$
80		0nn0	$⊢ 0 \in ℕ_{0}$
81	80	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}$
82	1 2 3 4 5 6 7 8 9 10 11 12	chfacfscmulcl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)})) \land 0 \in ℕ_{0}) \to (0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0) \in {Base}_{Y}$
83	81 82	mpd3an3	$⊢ ((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} G (0) \in {Base}_{Y}$
84		oveq1	$⊢ i = 0 \to i \underset{˙}{\times} X = 0 \underset{˙}{\times} X$
85		fveq2	$⊢ i = 0 \to G (i) = G (0)$
86	84 85	oveq12d	$⊢ i = 0 \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) = (0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0)$
87	14 86	gsumsn	$⊢ (Y \in Mnd \land 0 \in ℕ_{0} \land (0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0) \in {Base}_{Y}) \to \underset{i \in \{0\}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = (0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0)$
88	79 81 83 87	syl3anc	$⊢ ((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} G (i)) = (0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0)$
89	88	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} G (i))) \underset{˙}{+} (\underset{i \in \{0\}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0))$
90	78 89	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} G (i)) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0))$
91		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 \in V$
92		1nn0	$⊢ 1 \in ℕ_{0}$
93	92	a1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1 \in ℕ_{0}$
94	74 93	nn0addcld	$⊢ ((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}$
95	1 2 3 4 5 6 7 8 9 10 11 12	chfacfscmulcl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)})) \land s + 1 \in ℕ_{0}) \to ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1) \in {Base}_{Y}$
96	94 95	mpd3an3	$⊢ ((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} G (s + 1) \in {Base}_{Y}$
97		oveq1	$⊢ i = s + 1 \to i \underset{˙}{\times} X = (s + 1) \underset{˙}{\times} X$
98		fveq2	$⊢ i = s + 1 \to G (i) = G (s + 1)$
99	97 98	oveq12d	$⊢ i = s + 1 \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) = ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)$
100	14 99	gsumsn	$⊢ (Y \in Mnd \land s + 1 \in V \land ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1) \in {Base}_{Y}) \to \underset{i \in \{s + 1\}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)$
101	79 91 96 100	syl3anc	$⊢ ((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\}}{\sum_{Y}} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) = ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)$
102	90 101	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 \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (\underset{i \in \{s + 1\}}{\sum_{Y}}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) = (({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1))$
103		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$
104		simpll	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (N \in Fin \land R \in CRing \land M \in B)$
105		simplr	$⊢ (((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 (s \in ℕ \land b \in (B^{(0 \dots s)}))$
106		elfznn	$⊢ i \in (1 \dots s) \to i \in ℕ$
107	106	nnnn0d	$⊢ i \in (1 \dots s) \to i \in ℕ_{0}$
108	107	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}$
109	104 105 108 29	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} G (i) \in {Base}_{Y}$
110	109	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} G (i) \in {Base}_{Y}$
111	14 22 103 110	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} G (i)) \in {Base}_{Y}$
112	14 13	mndass	$⊢ (Y \in Mnd \land ({\sum_{Y}}_{i = 1}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i)) \in {Base}_{Y} \land (0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0) \in {Base}_{Y} \land ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1) \in {Base}_{Y})) \to (({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0)) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)))$
113	79 111 83 96 112	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} G (i))) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)) = ({\sum_{Y}}_{i = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0)) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)))$
114	106	nnne0d	$⊢ i \in (1 \dots s) \to i \neq 0$
115	114	ad2antlr	$⊢ ((((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)) \land n = i) \to i \neq 0$
116		neeq1	$⊢ n = i \to (n \neq 0 \leftrightarrow i \neq 0)$
117	116	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)) \land n = i) \to (n \neq 0 \leftrightarrow i \neq 0)$
118	115 117	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 (1 \dots s)) \land n = i) \to n \neq 0$
119		eqneqall	$⊢ n = 0 \to (n \neq 0 \to \underset{˙}{0} = T (b (i - 1)))$
120	118 119	mpan9	$⊢ (((((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)) \land n = i) \land n = 0) \to \underset{˙}{0} = T (b (i - 1))$
121		simplr	$⊢ (((((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)) \land n = i) \land n = 0) \to n = i$
122		eqeq1	$⊢ 0 = n \to (0 = i \leftrightarrow n = i)$
123	122	eqcoms	$⊢ n = 0 \to (0 = i \leftrightarrow n = i)$
124	123	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)) \land n = i) \land n = 0) \to (0 = i \leftrightarrow n = i)$
125	121 124	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 (1 \dots s)) \land n = i) \land n = 0) \to 0 = i$
126	125	fveq2d	$⊢ (((((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)) \land n = i) \land n = 0) \to b (0) = b (i)$
127	126	fveq2d	$⊢ (((((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)) \land n = i) \land n = 0) \to T (b (0)) = T (b (i))$
128	127	oveq2d	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \land n = i) \land n = 0) \to T (M) \underset{˙}{\times} T (b (0)) = T (M) \underset{˙}{\times} T (b (i))$
129	120 128	oveq12d	$⊢ (((((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)) \land n = i) \land n = 0) \to \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))$
130		elfz2	$⊢ i \in (1 \dots s) \leftrightarrow ((1 \in ℤ \land s \in ℤ \land i \in ℤ) \land (1 \leq i \land i \leq s))$
131		zleltp1	$⊢ (i \in ℤ \land s \in ℤ) \to (i \leq s \leftrightarrow i < s + 1)$
132	131	ancoms	$⊢ (s \in ℤ \land i \in ℤ) \to (i \leq s \leftrightarrow i < s + 1)$
133	132	3adant1	$⊢ (1 \in ℤ \land s \in ℤ \land i \in ℤ) \to (i \leq s \leftrightarrow i < s + 1)$
134	133	biimpcd	$⊢ i \leq s \to ((1 \in ℤ \land s \in ℤ \land i \in ℤ) \to i < s + 1)$
135	134	adantl	$⊢ (1 \leq i \land i \leq s) \to ((1 \in ℤ \land s \in ℤ \land i \in ℤ) \to i < s + 1)$
136	135	impcom	$⊢ ((1 \in ℤ \land s \in ℤ \land i \in ℤ) \land (1 \leq i \land i \leq s)) \to i < s + 1$
137	136	orcd	$⊢ ((1 \in ℤ \land s \in ℤ \land i \in ℤ) \land (1 \leq i \land i \leq s)) \to (i < s + 1 \lor s + 1 < i)$
138		zre	$⊢ s \in ℤ \to s \in ℝ$
139		1red	$⊢ s \in ℤ \to 1 \in ℝ$
140	138 139	readdcld	$⊢ s \in ℤ \to s + 1 \in ℝ$
141		zre	$⊢ i \in ℤ \to i \in ℝ$
142	140 141	anim12ci	$⊢ (s \in ℤ \land i \in ℤ) \to (i \in ℝ \land s + 1 \in ℝ)$
143	142	3adant1	$⊢ (1 \in ℤ \land s \in ℤ \land i \in ℤ) \to (i \in ℝ \land s + 1 \in ℝ)$
144		lttri2	$⊢ (i \in ℝ \land s + 1 \in ℝ) \to (i \neq s + 1 \leftrightarrow (i < s + 1 \lor s + 1 < i))$
145	143 144	syl	$⊢ (1 \in ℤ \land s \in ℤ \land i \in ℤ) \to (i \neq s + 1 \leftrightarrow (i < s + 1 \lor s + 1 < i))$
146	145	adantr	$⊢ ((1 \in ℤ \land s \in ℤ \land i \in ℤ) \land (1 \leq i \land i \leq s)) \to (i \neq s + 1 \leftrightarrow (i < s + 1 \lor s + 1 < i))$
147	137 146	mpbird	$⊢ ((1 \in ℤ \land s \in ℤ \land i \in ℤ) \land (1 \leq i \land i \leq s)) \to i \neq s + 1$
148	130 147	sylbi	$⊢ i \in (1 \dots s) \to i \neq s + 1$
149	148	ad2antlr	$⊢ ((((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)) \land n = i) \to i \neq s + 1$
150		neeq1	$⊢ n = i \to (n \neq s + 1 \leftrightarrow i \neq s + 1)$
151	150	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)) \land n = i) \to (n \neq s + 1 \leftrightarrow i \neq s + 1)$
152	149 151	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 (1 \dots s)) \land n = i) \to n \neq s + 1$
153	152	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)) \land n = i) \land \neg n = 0) \to n \neq s + 1$
154	153	neneqd	$⊢ (((((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)) \land n = i) \land \neg n = 0) \to \neg n = s + 1$
155	154	pm2.21d	$⊢ (((((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)) \land n = i) \land \neg n = 0) \to (n = s + 1 \to T (b (s)) = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i))))$
156	155	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)) \land n = i) \land \neg n = 0) \land n = s + 1) \to T (b (s)) = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))$
157	106	nnred	$⊢ i \in (1 \dots s) \to i \in ℝ$
158		eleq1w	$⊢ n = i \to (n \in ℝ \leftrightarrow i \in ℝ)$
159	157 158	syl5ibrcom	$⊢ i \in (1 \dots s) \to (n = i \to n \in ℝ)$
160	159	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 (n = i \to n \in ℝ)$
161	160	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)) \land n = i) \to n \in ℝ$
162	74	nn0red	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s \in ℝ$
163	162	ad2antrr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \land n = i) \to s \in ℝ$
164		1red	$⊢ ((((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)) \land n = i) \to 1 \in ℝ$
165	163 164	readdcld	$⊢ ((((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)) \land n = i) \to s + 1 \in ℝ$
166	130 136	sylbi	$⊢ i \in (1 \dots s) \to i < s + 1$
167	166	ad2antlr	$⊢ ((((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)) \land n = i) \to i < s + 1$
168		breq1	$⊢ n = i \to (n < s + 1 \leftrightarrow i < s + 1)$
169	168	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)) \land n = i) \to (n < s + 1 \leftrightarrow i < s + 1)$
170	167 169	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 (1 \dots s)) \land n = i) \to n < s + 1$
171	161 165 170	ltnsymd	$⊢ ((((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)) \land n = i) \to \neg s + 1 < n$
172	171	pm2.21d	$⊢ ((((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)) \land n = i) \to (s + 1 < n \to \underset{˙}{0} = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i))))$
173	172	ad2antrr	$⊢ ((((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \to (s + 1 < n \to \underset{˙}{0} = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i))))$
174	173	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)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \land s + 1 < n) \to \underset{˙}{0} = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))$
175		simp-4r	$⊢ (((((((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)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \land \neg s + 1 < n) \to n = i$
176	175	fvoveq1d	$⊢ (((((((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)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \land \neg s + 1 < n) \to b (n - 1) = b (i - 1)$
177	176	fveq2d	$⊢ (((((((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)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \land \neg s + 1 < n) \to T (b (n - 1)) = T (b (i - 1))$
178	175	fveq2d	$⊢ (((((((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)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \land \neg s + 1 < n) \to b (n) = b (i)$
179	178	fveq2d	$⊢ (((((((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)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \land \neg s + 1 < n) \to T (b (n)) = T (b (i))$
180	179	oveq2d	$⊢ (((((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \land \neg s + 1 < n) \to T (M) \underset{˙}{\times} T (b (n)) = T (M) \underset{˙}{\times} T (b (i))$
181	177 180	oveq12d	$⊢ (((((((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)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \land \neg s + 1 < n) \to T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))) = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))$
182	174 181	ifeqda	$⊢ ((((((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)) \land n = i) \land \neg n = 0) \land \neg n = s + 1) \to if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))) = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))$
183	156 182	ifeqda	$⊢ (((((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)) \land n = i) \land \neg n = 0) \to if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))))) = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))$
184	129 183	ifeqda	$⊢ ((((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)) \land n = i) \to if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))) = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))$
185		ovexd	$⊢ (((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)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i))) \in V$
186	9 184 108 185	fvmptd2	$⊢ (((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 G (i) = T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))$
187	186	oveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land i \in (1 \dots s)) \to (i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i) = (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i))))$
188	187	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} G (i)) = (i \in (1 \dots s) ⟼ (i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))$
189	188	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} G (i)) = {\sum_{Y}}_{i = 1}^{s} ((i \underset{˙}{\times} X) \underset{˙}{\cdot} (T (b (i - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (i)))))$
190		nn0p1gt0	$⊢ s \in ℕ_{0} \to 0 < s + 1$
191		0red	$⊢ s \in ℕ_{0} \to 0 \in ℝ$
192		ltne	$⊢ (0 \in ℝ \land 0 < s + 1) \to s + 1 \neq 0$
193	191 192	sylan	$⊢ (s \in ℕ_{0} \land 0 < s + 1) \to s + 1 \neq 0$
194		neeq1	$⊢ n = s + 1 \to (n \neq 0 \leftrightarrow s + 1 \neq 0)$
195	193 194	syl5ibrcom	$⊢ (s \in ℕ_{0} \land 0 < s + 1) \to (n = s + 1 \to n \neq 0)$
196	34 190 195	syl2anc2	$⊢ s \in ℕ \to (n = s + 1 \to n \neq 0)$
197	196	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (n = s + 1 \to n \neq 0)$
198	197	imp	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n = s + 1) \to n \neq 0$
199		eqneqall	$⊢ n = 0 \to (n \neq 0 \to \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = T (b (s)))$
200	198 199	mpan9	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n = s + 1) \land n = 0) \to \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = T (b (s))$
201		iftrue	$⊢ n = s + 1 \to if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))))) = T (b (s))$
202	201	ad2antlr	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n = s + 1) \land \neg n = 0) \to if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n))))) = T (b (s))$
203	200 202	ifeqda	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n = s + 1) \to if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))) = T (b (s))$
204	74 35	syl	$⊢ ((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}$
205		fvexd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (b (s)) \in V$
206	9 203 204 205	fvmptd2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G (s + 1) = T (b (s))$
207	206	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} G (s + 1) = ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))$
208	15	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
209		eqid	$⊢ {Base}_{P} = {Base}_{P}$
210	10 3 209	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
211	208 210	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to X \in {Base}_{P}$
212		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
213	212 209	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
214		eqid	$⊢ 1_{P} = 1_{P}$
215	212 214	ringidval	$⊢ 1_{P} = 0_{{mulGrp}_{P}}$
216	213 215 12	mulg0	$⊢ X \in {Base}_{P} \to 0 \underset{˙}{\times} X = 1_{P}$
217	211 216	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0 \underset{˙}{\times} X = 1_{P}$
218	3	ply1crng	$⊢ R \in CRing \to P \in CRing$
219	218	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land P \in CRing)$
220	219	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land P \in CRing)$
221	4	matsca2	$⊢ (N \in Fin \land P \in CRing) \to P = Scalar (Y)$
222	220 221	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P = Scalar (Y)$
223	222	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 1_{P} = 1_{Scalar (Y)}$
224	217 223	eqtrd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 0 \underset{˙}{\times} X = 1_{Scalar (Y)}$
225	224	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_{Scalar (Y)}$
226	225	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} G (0) = 1_{Scalar (Y)} \underset{˙}{\cdot} G (0)$
227	3 4	pmatlmod	$⊢ (N \in Fin \land R \in Ring) \to Y \in LMod$
228	15 227	sylan2	$⊢ (N \in Fin \land R \in CRing) \to Y \in LMod$
229	228	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in LMod$
230	1 2 3 4 5 6 7 8 9	chfacfisf	$⊢ ((N \in Fin \land R \in Ring \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G : ℕ_{0} ⟶ {Base}_{Y}$
231	15 230	syl3anl2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G : ℕ_{0} ⟶ {Base}_{Y}$
232	231 81	ffvelrnd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G (0) \in {Base}_{Y}$
233		eqid	$⊢ Scalar (Y) = Scalar (Y)$
234		eqid	$⊢ 1_{Scalar (Y)} = 1_{Scalar (Y)}$
235	14 233 11 234	lmodvs1	$⊢ (Y \in LMod \land G (0) \in {Base}_{Y}) \to 1_{Scalar (Y)} \underset{˙}{\cdot} G (0) = G (0)$
236	229 232 235	syl2an2r	$⊢ ((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} G (0) = G (0)$
237		iftrue	$⊢ n = 0 \to if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))) = \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))$
238		ovexd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) \in V$
239	9 237 81 238	fvmptd3	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to G (0) = \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))$
240	226 236 239	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} G (0) = \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))$
241	207 240	oveq12d	$⊢ ((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} G (s + 1)) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0)) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} (\underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
242	14 13	cmncom	$⊢ (Y \in CMnd \land (0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0) \in {Base}_{Y} \land ((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1) \in {Base}_{Y}) \to ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0)) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0))$
243	22 83 96 242	syl3anc	$⊢ ((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} G (0)) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0))$
244		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
245	19 244	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Grp$
246	245	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$
247	207 96	eqeltrrd	$⊢ ((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}$
248	19	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$
249	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
250	15 249	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
251	250	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}$
252		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$
253	208	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$
254		elmapi	$⊢ b \in (B^{(0 \dots s)}) \to b : (0 \dots s) ⟶ B$
255	254	adantl	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b : (0 \dots s) ⟶ B$
256	255	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$
257		0elfz	$⊢ s \in ℕ_{0} \to 0 \in (0 \dots s)$
258	34 257	syl	$⊢ s \in ℕ \to 0 \in (0 \dots s)$
259	258	ad2antrl	$⊢ ((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 \dots s)$
260	256 259	ffvelrnd	$⊢ ((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$
261	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (0) \in B) \to T (b (0)) \in {Base}_{Y}$
262	252 253 260 261	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}$
263	14 5	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}$
264	248 251 262 263	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}$
265	14 7 6 13	grpsubadd0sub	$⊢ (Y \in Grp \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 (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} (\underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
266	246 247 264 265	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{˙}{-} (T (M) \underset{˙}{\times} T (b (0))) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{+} (\underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
267	241 243 266	3eqtr4d	$⊢ ((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} G (0)) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)) = (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))$
268	189 267	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 = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} (((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0)) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1))) = ({\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))))$
269	113 268	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 = 1}^{s}, ((i \underset{˙}{\times} X) \underset{˙}{\cdot} G (i))) \underset{˙}{+} ((0 \underset{˙}{\times} X) \underset{˙}{\cdot} G (0))) \underset{˙}{+} (((s + 1) \underset{˙}{\times} X) \underset{˙}{\cdot} G (s + 1)) = ({\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))))$
270	75 102 269	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 \underset{˙}{\times} X) \underset{˙}{\cdot} G (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))))$
271	40 73 270	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} G (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 chfacfscmulgsum

Proof