chfacfpmmulgsum

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

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

Proof

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

Metamath Proof Explorer

Theorem chfacfpmmulgsum

Proof