Theorem cayleyhamilton

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", see theorem 7.8 in Roman p. 170 (without proof!), or theorem 3.1 in Lang p. 561. In other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. This is Metamath 100 proof #49. (Contributed by Alexander van der Vekens, 25-Nov-2019)

	Ref	Expression
Hypotheses	cayleyhamilton.a	$$⊢A=N\mathrm{Mat}R$$
	cayleyhamilton.b	$$⊢B={\mathrm{Base}}_A$$
	cayleyhamilton.0	$$⊢\underset{\dot{}}{0}=0_A$$
	cayleyhamilton.c	$$⊢C=N\mathrm{CharPlyMat}R$$
	cayleyhamilton.k	$$⊢K={\mathrm{coe}}_1\left(C\left(M\right)\right)$$
	cayleyhamilton.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
	cayleyhamilton.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_A}$$
Assertion	cayleyhamilton	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \underset{n\in {\mathbb{N}}_0}{{\sum }_A}\left(K\left(n\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }M\right)\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		cayleyhamilton.a	$$⊢A=N\mathrm{Mat}R$$
2		cayleyhamilton.b	$$⊢B={\mathrm{Base}}_A$$
3		cayleyhamilton.0	$$⊢\underset{\dot{}}{0}=0_A$$
4		cayleyhamilton.c	$$⊢C=N\mathrm{CharPlyMat}R$$
5		cayleyhamilton.k	$$⊢K={\mathrm{coe}}_1\left(C\left(M\right)\right)$$
6		cayleyhamilton.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
7		cayleyhamilton.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_A}$$
8		eqid	$$⊢1_A=1_A$$
9		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
10		eqid	$$⊢N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)=N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)$$
11		eqid	$$⊢{\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}={\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
12		eqid	$$⊢{-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}={-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
13		eqid	$$⊢0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}=0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
14		eqid	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}$$
15		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}}={\cdot }_{{\mathrm{mulGrp}}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}}$$
16		eqid	$$⊢N\mathrm{matToPolyMat}R=N\mathrm{matToPolyMat}R$$
17		eqeq1	$$⊢l=n\to \left(l=0\leftrightarrow n=0\right)$$
18		eqeq1	$$⊢l=n\to \left(l=x+1\leftrightarrow n=x+1\right)$$
19		breq2	$$⊢l=n\to \left(x+1<l\leftrightarrow x+1<n\right)$$
20		fvoveq1	$$⊢l=n\to y\left(l-1\right)=y\left(n-1\right)$$
21	20	fveq2d	$$⊢l=n\to \left(N\mathrm{matToPolyMat}R\right)\left(y\left(l-1\right)\right)=\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n-1\right)\right)$$
22		2fveq3	$$⊢l=n\to \left(N\mathrm{matToPolyMat}R\right)\left(y\left(l\right)\right)=\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n\right)\right)$$
23	22	oveq2d	$$⊢l=n\to \left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l\right)\right)=\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n\right)\right)$$
24	21 23	oveq12d	$$⊢l=n\to \left(N\mathrm{matToPolyMat}R\right)\left(y\left(l-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l\right)\right)\right)=\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n\right)\right)\right)$$
25	19 24	ifbieq2d	$$⊢l=n\to if\left(x+1<l,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)},\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l\right)\right)\right)\right)=if\left(x+1<n,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)},\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n\right)\right)\right)\right)$$
26	18 25	ifbieq2d	$$⊢l=n\to if\left(l=x+1,\left(N\mathrm{matToPolyMat}R\right)\left(y\left(x\right)\right),if\left(x+1<l,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)},\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l\right)\right)\right)\right)\right)=if\left(n=x+1,\left(N\mathrm{matToPolyMat}R\right)\left(y\left(x\right)\right),if\left(x+1<n,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)},\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n\right)\right)\right)\right)\right)$$
27	17 26	ifbieq2d	$$⊢l=n\to if\left(l=0,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}{-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(0\right)\right)\right),if\left(l=x+1,\left(N\mathrm{matToPolyMat}R\right)\left(y\left(x\right)\right),if\left(x+1<l,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)},\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l\right)\right)\right)\right)\right)\right)=if\left(n=0,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}{-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(0\right)\right)\right),if\left(n=x+1,\left(N\mathrm{matToPolyMat}R\right)\left(y\left(x\right)\right),if\left(x+1<n,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)},\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n\right)\right)\right)\right)\right)\right)$$
28	27	cbvmptv	$$⊢\left(l\in {\mathbb{N}}_0⟼if\left(l=0,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}{-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(0\right)\right)\right),if\left(l=x+1,\left(N\mathrm{matToPolyMat}R\right)\left(y\left(x\right)\right),if\left(x+1<l,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)},\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(l\right)\right)\right)\right)\right)\right)\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}{-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(0\right)\right)\right),if\left(n=x+1,\left(N\mathrm{matToPolyMat}R\right)\left(y\left(x\right)\right),if\left(x+1<n,0_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)},\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n-1\right)\right){-}_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(\left(N\mathrm{matToPolyMat}R\right)\left(M\right){\cdot }_{\left(N\mathrm{Mat}{\mathrm{Poly}}_1\left(R\right)\right)}\left(N\mathrm{matToPolyMat}R\right)\left(y\left(n\right)\right)\right)\right)\right)\right)\right)$$
29		eqid	$$⊢N\mathrm{cPolyMatToMat}R=N\mathrm{cPolyMatToMat}R$$
30	1 2 3 8 6 7 4 5 9 10 11 12 13 14 15 16 28 29	cayleyhamilton0	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{CRing}\wedge M\in B\right)\to \underset{n\in {\mathbb{N}}_0}{{\sum }_A}\left(K\left(n\right)\underset{\dot{}}{\ast }\left(n\underset{\dot{}}{\times }M\right)\right)=\underset{\dot{}}{0}$$