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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	cayleyhamilton.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	cayleyhamilton.0	⊢ 0 = ( 0g ‘ 𝐴 )
	cayleyhamilton.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	cayleyhamilton.k	⊢ 𝐾 = ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) )
	cayleyhamilton.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	cayleyhamilton.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
Assertion	cayleyhamilton	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		cayleyhamilton.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		cayleyhamilton.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		cayleyhamilton.0	⊢ 0 = ( 0g ‘ 𝐴 )
4		cayleyhamilton.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
5		cayleyhamilton.k	⊢ 𝐾 = ( coe1 ‘ ( 𝐶 ‘ 𝑀 ) )
6		cayleyhamilton.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
7		cayleyhamilton.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
8		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
9		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
10		eqid	⊢ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) )
11		eqid	⊢ ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
12		eqid	⊢ ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
13		eqid	⊢ ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
14		eqid	⊢ ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) )
15		eqid	⊢ ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) )
16		eqid	⊢ ( 𝑁 matToPolyMat 𝑅 ) = ( 𝑁 matToPolyMat 𝑅 )
17		eqeq1	⊢ ( 𝑙 = 𝑛 → ( 𝑙 = 0 ↔ 𝑛 = 0 ) )
18		eqeq1	⊢ ( 𝑙 = 𝑛 → ( 𝑙 = ( 𝑥 + 1 ) ↔ 𝑛 = ( 𝑥 + 1 ) ) )
19		breq2	⊢ ( 𝑙 = 𝑛 → ( ( 𝑥 + 1 ) < 𝑙 ↔ ( 𝑥 + 1 ) < 𝑛 ) )
20		fvoveq1	⊢ ( 𝑙 = 𝑛 → ( 𝑦 ‘ ( 𝑙 − 1 ) ) = ( 𝑦 ‘ ( 𝑛 − 1 ) ) )
21	20	fveq2d	⊢ ( 𝑙 = 𝑛 → ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑙 − 1 ) ) ) = ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑛 − 1 ) ) ) )
22		2fveq3	⊢ ( 𝑙 = 𝑛 → ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑙 ) ) = ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑛 ) ) )
23	22	oveq2d	⊢ ( 𝑙 = 𝑛 → ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑙 ) ) ) = ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑛 ) ) ) )
24	21 23	oveq12d	⊢ ( 𝑙 = 𝑛 → ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑙 ) ) ) ) = ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) )
25	19 24	ifbieq2d	⊢ ( 𝑙 = 𝑛 → if ( ( 𝑥 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑙 ) ) ) ) ) = if ( ( 𝑥 + 1 ) < 𝑛 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) )
26	18 25	ifbieq2d	⊢ ( 𝑙 = 𝑛 → if ( 𝑙 = ( 𝑥 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑥 ) ) , if ( ( 𝑥 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑙 ) ) ) ) ) ) = if ( 𝑛 = ( 𝑥 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑥 ) ) , if ( ( 𝑥 + 1 ) < 𝑛 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) )
27	17 26	ifbieq2d	⊢ ( 𝑙 = 𝑛 → if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑥 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑥 ) ) , if ( ( 𝑥 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑙 ) ) ) ) ) ) ) = if ( 𝑛 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑥 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑥 ) ) , if ( ( 𝑥 + 1 ) < 𝑛 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ) )
28	27	cbvmptv	⊢ ( 𝑙 ∈ ℕ0 ↦ if ( 𝑙 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 0 ) ) ) ) , if ( 𝑙 = ( 𝑥 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑥 ) ) , if ( ( 𝑥 + 1 ) < 𝑙 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑙 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑙 ) ) ) ) ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑥 + 1 ) , ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑥 ) ) , if ( ( 𝑥 + 1 ) < 𝑛 , ( 0g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) , ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ ( 𝑛 − 1 ) ) ) ( -g ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ( .r ‘ ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ ( 𝑦 ‘ 𝑛 ) ) ) ) ) ) ) )
29		eqid	⊢ ( 𝑁 cPolyMatToMat 𝑅 ) = ( 𝑁 cPolyMatToMat 𝑅 )
30	1 2 3 8 6 7 4 5 9 10 11 12 13 14 15 16 28 29	cayleyhamilton0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐾 ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = 0 )