cayhamlem1

	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}}$
Assertion	cayhamlem1	$⊢ ((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)) = \underset{˙}{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		eqid	$⊢ +_{Y} = +_{Y}$
12	1 2 3 4 5 6 7 8 9 10 11	chfacfpmmulgsum2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{i \in ℕ_{0}}{\sum_{Y}} ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} G (i)) = ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))))) +_{Y} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
13		elfzelz	$⊢ i \in (1 \dots s) \to i \in ℤ$
14	13	zcnd	$⊢ i \in (1 \dots s) \to i \in ℂ$
15		pncan1	$⊢ i \in ℂ \to i + 1 - 1 = i$
16	14 15	syl	$⊢ i \in (1 \dots s) \to i + 1 - 1 = i$
17	16	eqcomd	$⊢ i \in (1 \dots s) \to i = i + 1 - 1$
18	17	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land i \in (1 \dots s)) \to i = i + 1 - 1$
19	18	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land i \in (1 \dots s)) \to b (i) = b (i + 1 - 1)$
20	19	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land i \in (1 \dots s)) \to T (b (i)) = T (b (i + 1 - 1))$
21	20	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land i \in (1 \dots s)) \to ((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)) = ((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i + 1 - 1))$
22	21	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land i \in (1 \dots s)) \to ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))) = ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i + 1 - 1)))$
23	22	mpteq2dva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (i \in (1 \dots s) ⟼ ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)))) = (i \in (1 \dots s) ⟼ ((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i + 1 - 1))))$
24	23	oveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)))) = {\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i + 1 - 1))))$
25	24	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)))) = {\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i + 1 - 1))))$
26		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
27		crngring	$⊢ R \in CRing \to R \in Ring$
28	27	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
29	28	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
30	3 4	pmatring	$⊢ (N \in Fin \land R \in Ring) \to Y \in Ring$
31	29 30	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
32		ringabl	$⊢ Y \in Ring \to Y \in Abel$
33	31 32	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Abel$
34	33	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to Y \in Abel$
35		elnnuz	$⊢ s \in ℕ \leftrightarrow s \in ℤ_{\geq 1}$
36	35	biimpi	$⊢ s \in ℕ \to s \in ℤ_{\geq 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 s \in ℤ_{\geq 1}$
38	31	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$
39	38	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to Y \in Ring$
40	28 30	syl	$⊢ (N \in Fin \land R \in CRing) \to Y \in Ring$
41	40	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Ring$
42		eqid	$⊢ {mulGrp}_{Y} = {mulGrp}_{Y}$
43	42	ringmgp	$⊢ Y \in Ring \to {mulGrp}_{Y} \in Mnd$
44	41 43	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{Y} \in Mnd$
45	44	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {mulGrp}_{Y} \in Mnd$
46	45	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to {mulGrp}_{Y} \in Mnd$
47		mndmgm	$⊢ {mulGrp}_{Y} \in Mnd \to {mulGrp}_{Y} \in Mgm$
48	46 47	syl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to {mulGrp}_{Y} \in Mgm$
49		elfznn	$⊢ k \in (1 \dots s + 1) \to k \in ℕ$
50	49	adantl	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to k \in ℕ$
51	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land M \in B) \to T (M) \in {Base}_{Y}$
52	27 51	syl3an2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to T (M) \in {Base}_{Y}$
53	52	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}$
54	53	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to T (M) \in {Base}_{Y}$
55	42 26	mgpbas	$⊢ {Base}_{Y} = {Base}_{{mulGrp}_{Y}}$
56	55 10	mulgnncl	$⊢ ({mulGrp}_{Y} \in Mgm \land k \in ℕ \land T (M) \in {Base}_{Y}) \to k \underset{˙}{\times} T (M) \in {Base}_{Y}$
57	48 50 54 56	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to k \underset{˙}{\times} T (M) \in {Base}_{Y}$
58		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$
59	58	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to N \in Fin$
60	27	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
61	60	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$
62	61	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to R \in Ring$
63		elmapi	$⊢ b \in (B^{(0 \dots s)}) \to b : (0 \dots s) ⟶ B$
64	63	adantl	$⊢ (s \in ℕ \land b \in (B^{(0 \dots s)})) \to b : (0 \dots s) ⟶ B$
65	64	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$
66	65	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to b : (0 \dots s) ⟶ B$
67		nnz	$⊢ k \in ℕ \to k \in ℤ$
68		peano2nn	$⊢ s \in ℕ \to s + 1 \in ℕ$
69	68	nnzd	$⊢ s \in ℕ \to s + 1 \in ℤ$
70		elfzm1b	$⊢ (k \in ℤ \land s + 1 \in ℤ) \to (k \in (1 \dots s + 1) \leftrightarrow k - 1 \in (0 \dots s + 1 - 1))$
71	67 69 70	syl2an	$⊢ (k \in ℕ \land s \in ℕ) \to (k \in (1 \dots s + 1) \leftrightarrow k - 1 \in (0 \dots s + 1 - 1))$
72		nncn	$⊢ s \in ℕ \to s \in ℂ$
73		pncan1	$⊢ s \in ℂ \to s + 1 - 1 = s$
74	72 73	syl	$⊢ s \in ℕ \to s + 1 - 1 = s$
75	74	adantl	$⊢ (k \in ℕ \land s \in ℕ) \to s + 1 - 1 = s$
76	75	oveq2d	$⊢ (k \in ℕ \land s \in ℕ) \to (0 \dots s + 1 - 1) = (0 \dots s)$
77	76	eleq2d	$⊢ (k \in ℕ \land s \in ℕ) \to (k - 1 \in (0 \dots s + 1 - 1) \leftrightarrow k - 1 \in (0 \dots s))$
78	77	biimpd	$⊢ (k \in ℕ \land s \in ℕ) \to (k - 1 \in (0 \dots s + 1 - 1) \to k - 1 \in (0 \dots s))$
79	71 78	sylbid	$⊢ (k \in ℕ \land s \in ℕ) \to (k \in (1 \dots s + 1) \to k - 1 \in (0 \dots s))$
80	79	expcom	$⊢ s \in ℕ \to (k \in ℕ \to (k \in (1 \dots s + 1) \to k - 1 \in (0 \dots s)))$
81	80	com13	$⊢ k \in (1 \dots s + 1) \to (k \in ℕ \to (s \in ℕ \to k - 1 \in (0 \dots s)))$
82	49 81	mpd	$⊢ k \in (1 \dots s + 1) \to (s \in ℕ \to k - 1 \in (0 \dots s))$
83	82	com12	$⊢ s \in ℕ \to (k \in (1 \dots s + 1) \to k - 1 \in (0 \dots s))$
84	83	ad2antrl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (k \in (1 \dots s + 1) \to k - 1 \in (0 \dots s))$
85	84	imp	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to k - 1 \in (0 \dots s)$
86	66 85	ffvelrnd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to b (k - 1) \in B$
87	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (k - 1) \in B) \to T (b (k - 1)) \in {Base}_{Y}$
88	59 62 86 87	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to T (b (k - 1)) \in {Base}_{Y}$
89	26 5	ringcl	$⊢ (Y \in Ring \land k \underset{˙}{\times} T (M) \in {Base}_{Y} \land T (b (k - 1)) \in {Base}_{Y}) \to (k \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (k - 1)) \in {Base}_{Y}$
90	39 57 88 89	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land k \in (1 \dots s + 1)) \to (k \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (k - 1)) \in {Base}_{Y}$
91	90	ralrimiva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \forall k \in (1 \dots s + 1) (k \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (k - 1)) \in {Base}_{Y}$
92		oveq1	$⊢ k = i \to k \underset{˙}{\times} T (M) = i \underset{˙}{\times} T (M)$
93		fvoveq1	$⊢ k = i \to b (k - 1) = b (i - 1)$
94	93	fveq2d	$⊢ k = i \to T (b (k - 1)) = T (b (i - 1))$
95	92 94	oveq12d	$⊢ k = i \to (k \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (k - 1)) = (i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))$
96		oveq1	$⊢ k = i + 1 \to k \underset{˙}{\times} T (M) = (i + 1) \underset{˙}{\times} T (M)$
97		fvoveq1	$⊢ k = i + 1 \to b (k - 1) = b (i + 1 - 1)$
98	97	fveq2d	$⊢ k = i + 1 \to T (b (k - 1)) = T (b (i + 1 - 1))$
99	96 98	oveq12d	$⊢ k = i + 1 \to (k \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (k - 1)) = ((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i + 1 - 1))$
100		oveq1	$⊢ k = 1 \to k \underset{˙}{\times} T (M) = 1 \underset{˙}{\times} T (M)$
101		fvoveq1	$⊢ k = 1 \to b (k - 1) = b (1 - 1)$
102	101	fveq2d	$⊢ k = 1 \to T (b (k - 1)) = T (b (1 - 1))$
103	100 102	oveq12d	$⊢ k = 1 \to (k \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (k - 1)) = (1 \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (1 - 1))$
104		oveq1	$⊢ k = s + 1 \to k \underset{˙}{\times} T (M) = (s + 1) \underset{˙}{\times} T (M)$
105		fvoveq1	$⊢ k = s + 1 \to b (k - 1) = b (s + 1 - 1)$
106	105	fveq2d	$⊢ k = s + 1 \to T (b (k - 1)) = T (b (s + 1 - 1))$
107	104 106	oveq12d	$⊢ k = s + 1 \to (k \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (k - 1)) = ((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s + 1 - 1))$
108	26 34 6 37 91 95 99 103 107	telgsumfz	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {\sum_{Y}}_{i = 1}^{s} (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i + 1 - 1)))) = ((1 \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (1 - 1))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s + 1 - 1)))$
109	25 108	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} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i)))) = ((1 \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (1 - 1))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s + 1 - 1)))$
110	109	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ({\sum_{Y}}_{i = 1}^{s}, (((i \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i - 1))) \underset{˙}{-} (((i + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (i))))) +_{Y} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))) = (((1 \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (1 - 1))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s + 1 - 1)))) +_{Y} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
111	55 10	mulg1	$⊢ T (M) \in {Base}_{Y} \to 1 \underset{˙}{\times} T (M) = T (M)$
112	52 111	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to 1 \underset{˙}{\times} T (M) = T (M)$
113	112	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1 \underset{˙}{\times} T (M) = T (M)$
114		1cnd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1 \in ℂ$
115	114	subidd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to 1 - 1 = 0$
116	115	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to b (1 - 1) = b (0)$
117	116	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to T (b (1 - 1)) = T (b (0))$
118	113 117	oveq12d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (1 \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (1 - 1)) = T (M) \underset{˙}{\times} T (b (0))$
119	72	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 ℂ$
120	119 114	pncand	$⊢ ((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$
121	120	fveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to b (s + 1 - 1) = b (s)$
122	121	fveq2d	$⊢ ((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 + 1 - 1)) = T (b (s))$
123	122	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} T (b (s + 1 - 1)) = ((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))$
124	118 123	oveq12d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to ((1 \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (1 - 1))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s + 1 - 1))) = (T (M) \underset{˙}{\times} T (b (0))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s)))$
125	124	oveq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (((1 \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (1 - 1))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s + 1 - 1)))) +_{Y} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))) = ((T (M) \underset{˙}{\times} T (b (0))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s)))) +_{Y} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))))$
126		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
127	31 126	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Y \in Grp$
128	127	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$
129		nnnn0	$⊢ s \in ℕ \to s \in ℕ_{0}$
130		0elfz	$⊢ s \in ℕ_{0} \to 0 \in (0 \dots s)$
131	129 130	syl	$⊢ s \in ℕ \to 0 \in (0 \dots s)$
132	131	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)$
133	65 132	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$
134	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}$
135	58 61 133 134	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}$
136	26 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}$
137	38 53 135 136	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}$
138	45 47	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to {mulGrp}_{Y} \in Mgm$
139		simprl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to s \in ℕ$
140	139	peano2nnd	$⊢ ((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 ℕ$
141	55 10	mulgnncl	$⊢ ({mulGrp}_{Y} \in Mgm \land s + 1 \in ℕ \land T (M) \in {Base}_{Y}) \to (s + 1) \underset{˙}{\times} T (M) \in {Base}_{Y}$
142	138 140 53 141	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) \in {Base}_{Y}$
143		nn0fz0	$⊢ s \in ℕ_{0} \leftrightarrow s \in (0 \dots s)$
144	129 143	sylib	$⊢ s \in ℕ \to s \in (0 \dots s)$
145	144	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 \dots s)$
146	65 145	ffvelrnd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to b (s) \in B$
147	8 1 2 3 4	mat2pmatbas	$⊢ (N \in Fin \land R \in Ring \land b (s) \in B) \to T (b (s)) \in {Base}_{Y}$
148	58 61 146 147	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 (s)) \in {Base}_{Y}$
149	26 5	ringcl	$⊢ (Y \in Ring \land (s + 1) \underset{˙}{\times} T (M) \in {Base}_{Y} \land T (b (s)) \in {Base}_{Y}) \to ((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s)) \in {Base}_{Y}$
150	38 142 148 149	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)) \in {Base}_{Y}$
151	26 11 6 7	grpnpncan0	$⊢ (Y \in Grp \land (T (M) \underset{˙}{\times} T (b (0)) \in {Base}_{Y} \land ((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s)) \in {Base}_{Y})) \to ((T (M) \underset{˙}{\times} T (b (0))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s)))) +_{Y} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))) = \underset{˙}{0}$
152	128 137 150 151	syl12anc	$⊢ ((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))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s)))) +_{Y} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))) = \underset{˙}{0}$
153	125 152	eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (((1 \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (1 - 1))) \underset{˙}{-} (((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s + 1 - 1)))) +_{Y} ((((s + 1) \underset{˙}{\times} T (M)) \underset{˙}{\times} T (b (s))) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0)))) = \underset{˙}{0}$
154	12 110 153	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)) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem cayhamlem1

Proof