cayleyhamilton0

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton provides definitions not used in the theorem itself, but in its proof to make it clearer, more readable and shorter compared with a proof without them (see cayleyhamiltonALT )! (Contributed by AV, 25-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	cayleyhamilton0.a	$⊢ A = N Mat R$
	cayleyhamilton0.b	$⊢ B = {Base}_{A}$
	cayleyhamilton0.0	$⊢ \underset{˙}{0} = 0_{A}$
	cayleyhamilton0.1	$⊢ \underset{˙}{1} = 1_{A}$
	cayleyhamilton0.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	cayleyhamilton0.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
	cayleyhamilton0.c	$⊢ C = N CharPlyMat R$
	cayleyhamilton0.k	$⊢ K = {coe}_{1} (C (M))$
	cayleyhamilton0.p	$⊢ P = {Poly}_{1} (R)$
	cayleyhamilton0.y	$⊢ Y = N Mat P$
	cayleyhamilton0.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	cayleyhamilton0.s	$⊢ \underset{˙}{-} = -_{Y}$
	cayleyhamilton0.z	$⊢ Z = 0_{Y}$
	cayleyhamilton0.w	$⊢ W = {Base}_{Y}$
	cayleyhamilton0.e2	$⊢ E = \cdot_{{mulGrp}_{Y}}$
	cayleyhamilton0.t	$⊢ T = N matToPolyMat R$
	cayleyhamilton0.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, Z \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, Z, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
	cayleyhamilton0.u	$⊢ U = N cPolyMatToMat R$
Assertion	cayleyhamilton0	$⊢ (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		cayleyhamilton0.a	$⊢ A = N Mat R$
2		cayleyhamilton0.b	$⊢ B = {Base}_{A}$
3		cayleyhamilton0.0	$⊢ \underset{˙}{0} = 0_{A}$
4		cayleyhamilton0.1	$⊢ \underset{˙}{1} = 1_{A}$
5		cayleyhamilton0.m	$⊢ \underset{˙}{*} = \cdot_{A}$
6		cayleyhamilton0.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
7		cayleyhamilton0.c	$⊢ C = N CharPlyMat R$
8		cayleyhamilton0.k	$⊢ K = {coe}_{1} (C (M))$
9		cayleyhamilton0.p	$⊢ P = {Poly}_{1} (R)$
10		cayleyhamilton0.y	$⊢ Y = N Mat P$
11		cayleyhamilton0.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
12		cayleyhamilton0.s	$⊢ \underset{˙}{-} = -_{Y}$
13		cayleyhamilton0.z	$⊢ Z = 0_{Y}$
14		cayleyhamilton0.w	$⊢ W = {Base}_{Y}$
15		cayleyhamilton0.e2	$⊢ E = \cdot_{{mulGrp}_{Y}}$
16		cayleyhamilton0.t	$⊢ T = N matToPolyMat R$
17		cayleyhamilton0.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, Z \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, Z, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
18		cayleyhamilton0.u	$⊢ U = N cPolyMatToMat R$
19		eqid	$⊢ C (M) = C (M)$
20	1 2 9 10 11 12 13 16 7 19 17 14 4 5 18 6 15	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)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))$
21	8	eqcomi	$⊢ {coe}_{1} (C (M)) = K$
22	21	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$
23	22	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)$
24	23	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)$
25	24	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))$
26	25	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))$
27	26	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)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))) \leftrightarrow \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))))$
28	27	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)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))$
29		oveq1	$⊢ n = l \to n E T (M) = l E T (M)$
30		fveq2	$⊢ n = l \to G (n) = G (l)$
31	29 30	oveq12d	$⊢ n = l \to (n E T (M)) \underset{˙}{\times} G (n) = (l E T (M)) \underset{˙}{\times} G (l)$
32	31	cbvmptv	$⊢ (n \in ℕ_{0} ⟼ (n E T (M)) \underset{˙}{\times} G (n)) = (l \in ℕ_{0} ⟼ (l E T (M)) \underset{˙}{\times} G (l))$
33	32	oveq2i	$⊢ \underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)) = \underset{l \in ℕ_{0}}{\sum_{Y}} ((l E T (M)) \underset{˙}{\times} G (l))$
34	1 2 9 10 11 12 13 16 17 15	cayhamlem1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to \underset{l \in ℕ_{0}}{\sum_{Y}} ((l E T (M)) \underset{˙}{\times} G (l)) = Z$
35	33 34	eqtrid	$⊢ ((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_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)) = Z$
36		fveq2	$⊢ \underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)) = Z \to U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))) = U (Z)$
37		crngring	$⊢ R \in CRing \to R \in Ring$
38	37	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
39	38	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
40		eqid	$⊢ 0_{A} = 0_{A}$
41	1 18 9 10 40 13	m2cpminv0	$⊢ (N \in Fin \land R \in Ring) \to U (Z) = 0_{A}$
42	39 41	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to U (Z) = 0_{A}$
43	42 3	eqtr4di	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to U (Z) = \underset{˙}{0}$
44	43	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to U (Z) = \underset{˙}{0}$
45	36 44	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_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)) = Z) \to U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))) = \underset{˙}{0}$
46	35 45	mpdan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (s \in ℕ \land b \in (B^{(0 \dots s)}))) \to U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))) = \underset{˙}{0}$
47	46	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)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))) \to U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))) = \underset{˙}{0}$
48	28 47	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)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n)))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0}$
49	48	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)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0})$
50	49	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)) = U (\underset{n \in ℕ_{0}}{\sum_{Y}} ((n E T (M)) \underset{˙}{\times} G (n))) \to \underset{n \in ℕ_{0}}{\sum_{A}} (K (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{˙}{0})$
51	20 50	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 cayleyhamilton0

Proof