cayleyhamiltonALT

Description: Alternate proof of cayleyhamilton , the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 directly, but has the same structure as the proof of cayleyhamilton0 . In contrast to the proof of cayleyhamilton0 , only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	cayleyhamilton.a	$⊢ A = N Mat R$
	cayleyhamilton.b	$⊢ B = {Base}_{A}$
	cayleyhamilton.0	$⊢ \underset{˙}{0} = 0_{A}$
	cayleyhamilton.c	$⊢ C = N CharPlyMat R$
	cayleyhamilton.k	$⊢ K = {coe}_{1} (C (M))$
	cayleyhamilton.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	cayleyhamilton.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
Assertion	cayleyhamiltonALT	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		cayleyhamilton.a	$⊢ A = N Mat R$
2		cayleyhamilton.b	$⊢ B = {Base}_{A}$
3		cayleyhamilton.0	$⊢ \underset{˙}{0} = 0_{A}$
4		cayleyhamilton.c	$⊢ C = N CharPlyMat R$
5		cayleyhamilton.k	$⊢ K = {coe}_{1} (C (M))$
6		cayleyhamilton.m	$⊢ \underset{˙}{*} = \cdot_{A}$
7		cayleyhamilton.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
8		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
9		eqid	$⊢ N Mat {Poly}_{1} (R) = N Mat {Poly}_{1} (R)$
10		eqid	$⊢ \cdot_{(N Mat {Poly}_{1} (R))} = \cdot_{(N Mat {Poly}_{1} (R))}$
11		eqid	$⊢ -_{(N Mat {Poly}_{1} (R))} = -_{(N Mat {Poly}_{1} (R))}$
12		eqid	$⊢ 0_{(N Mat {Poly}_{1} (R))} = 0_{(N Mat {Poly}_{1} (R))}$
13		eqid	$⊢ N matToPolyMat R = N matToPolyMat R$
14		eqid	$⊢ C (M) = C (M)$
15		eqeq1	$⊢ l = n \to (l = 0 \leftrightarrow n = 0)$
16		eqeq1	$⊢ l = n \to (l = s + 1 \leftrightarrow n = s + 1)$
17		breq2	$⊢ l = n \to (s + 1 < l \leftrightarrow s + 1 < n)$
18		oveq1	$⊢ l = n \to l - 1 = n - 1$
19	18	fveq2d	$⊢ l = n \to b (l - 1) = b (n - 1)$
20	19	fveq2d	$⊢ l = n \to (N matToPolyMat R) (b (l - 1)) = (N matToPolyMat R) (b (n - 1))$
21		fveq2	$⊢ l = n \to b (l) = b (n)$
22	21	fveq2d	$⊢ l = n \to (N matToPolyMat R) (b (l)) = (N matToPolyMat R) (b (n))$
23	22	oveq2d	$⊢ l = n \to (N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l)) = (N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (n))$
24	20 23	oveq12d	$⊢ l = n \to (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))) = (N matToPolyMat R) (b (n - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (n)))$
25	17 24	ifbieq2d	$⊢ l = n \to if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l)))) = if (s + 1 < n, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (n - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (n))))$
26	16 25	ifbieq2d	$⊢ l = n \to if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))) = if (n = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < n, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (n - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (n)))))$
27	15 26	ifbieq2d	$⊢ l = n \to if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l)))))) = if (n = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (n = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < n, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (n - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (n))))))$
28	27	cbvmptv	$⊢ (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) = (n \in ℕ_{0} ⟼ if (n = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (n = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < n, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (n - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (n)))))))$
29		eqid	$⊢ {Base}_{(N Mat {Poly}_{1} (R))} = {Base}_{(N Mat {Poly}_{1} (R))}$
30		eqid	$⊢ 1_{A} = 1_{A}$
31		eqid	$⊢ N cPolyMatToMat R = N cPolyMatToMat R$
32		eqid	$⊢ \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} = \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}}$
33	1 2 8 9 10 11 12 13 4 14 28 29 30 6 31 7 32	cayhamlem4	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = (N cPolyMatToMat R) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)))$
34		eqid	$⊢ N ConstPolyMat R = N ConstPolyMat R$
35	31 34	cpm2mfval	$⊢ (N \in Fin \land R \in CRing) \to N cPolyMatToMat R = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0)))$
36	35	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) = N cPolyMatToMat R$
37	36	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) = N cPolyMatToMat R$
38	37	fveq1d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) = (N cPolyMatToMat R) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)))$
39	38	eqeq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) \leftrightarrow \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (N cPolyMatToMat R) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))))$
40	39	2rexbidv	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) \leftrightarrow \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (N cPolyMatToMat R) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))))$
41	33 40	mpbird	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)))$
42	5	eqcomi	$⊢ {coe}_{1} (C (M)) = K$
43	42	a1i	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \to {coe}_{1} (C (M)) = K$
44	43	fveq1d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \to {coe}_{1} (C (M)) (n) = K (n)$
45	44	oveq1d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land n \in ℕ_{0}) \to {coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M) = K (n) \underset{˙}{} (n \underset{˙}{\times} M)$
46	45	mpteq2dva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (n \in ℕ_{0} ⟼ {coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (n \in ℕ_{0} ⟼ K (n) \underset{˙}{} (n \underset{˙}{\times} M))$
47	46	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M))$
48	47	eqeq1d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (\underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) \leftrightarrow \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))))$
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 \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)))$
50		oveq1	$⊢ n = j \to n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M) = j \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)$
51		fveq2	$⊢ n = j \to (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n) = (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (j)$
52	50 51	oveq12d	$⊢ n = j \to (n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n) = (j \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (j)$
53	52	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ (n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)) = (j \in ℕ_{0} ⟼ (j \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (j))$
54	53	oveq2i	$⊢ \underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)) = \underset{j \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((j \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (j))$
55	54	a1i	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)) = \underset{j \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((j \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (j))$
56	1 2 8 9 10 11 12 13 28 32	cayhamlem1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{j \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((j \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (j)) = 0_{(N Mat {Poly}_{1} (R))}$
57	55 56	eqtrd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)) = 0_{(N Mat {Poly}_{1} (R))}$
58		fveq2	$⊢ \underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)) = 0_{(N Mat {Poly}_{1} (R))} \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (0_{(N Mat {Poly}_{1} (R))})$
59		crngring	$⊢ R \in CRing \to R \in Ring$
60	59	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
61	60	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
62	31 34	cpm2mfval	$⊢ (N \in Fin \land R \in Ring) \to N cPolyMatToMat R = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0)))$
63	62	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) = N cPolyMatToMat R$
64	63	fveq1d	$⊢ (N \in Fin \land R \in Ring) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (0_{(N Mat {Poly}_{1} (R))}) = (N cPolyMatToMat R) (0_{(N Mat {Poly}_{1} (R))})$
65		eqid	$⊢ 0_{A} = 0_{A}$
66	1 31 8 9 65 12	m2cpminv0	$⊢ (N \in Fin \land R \in Ring) \to (N cPolyMatToMat R) (0_{(N Mat {Poly}_{1} (R))}) = 0_{A}$
67	64 66	eqtrd	$⊢ (N \in Fin \land R \in Ring) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (0_{(N Mat {Poly}_{1} (R))}) = 0_{A}$
68	61 67	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (0_{(N Mat {Poly}_{1} (R))}) = 0_{A}$
69	68 3	eqtr4di	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (0_{(N Mat {Poly}_{1} (R))}) = \underset{˙}{0}$
70	69	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (0_{(N Mat {Poly}_{1} (R))}) = \underset{˙}{0}$
71	58 70	sylan9eqr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land \underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)) = 0_{(N Mat {Poly}_{1} (R))}) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) = \underset{˙}{0}$
72	57 71	mpdan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) = \underset{˙}{0}$
73	72	adantr	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)))) \to (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) = \underset{˙}{0}$
74	49 73	eqtrd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \land \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n)))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0}$
75	74	ex	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to (\underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0})$
76	75	rexlimdvva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (C (M)) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (m \in (N ConstPolyMat R) ⟼ (x \in N, y \in N ⟼ {coe}_{1} (x m y) (0))) (\underset{n \in ℕ_{0}}{\sum_{N Mat {Poly}_{1} (R)}} ((n \cdot_{{mulGrp}_{(N Mat {Poly}_{1} (R))}} (N matToPolyMat R) (M)) \cdot_{(N Mat {Poly}_{1} (R))} (l \in ℕ_{0} ⟼ if (l = 0, 0_{(N Mat {Poly}_{1} (R))} -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (0))), if (l = s + 1, (N matToPolyMat R) (b (s)), if (s + 1 < l, 0_{(N Mat {Poly}_{1} (R))}, (N matToPolyMat R) (b (l - 1)) -_{(N Mat {Poly}_{1} (R))} ((N matToPolyMat R) (M) \cdot_{(N Mat {Poly}_{1} (R))} (N matToPolyMat R) (b (l))))))) (n))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0})$
77	41 76	mpd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem cayleyhamiltonALT

Proof