Metamath Proof Explorer

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 Mat R )
cayleyhamilton.b 
|- B = ( Base ` A )
cayleyhamilton.0 
|- .0. = ( 0g ` A )
cayleyhamilton.c 
|- C = ( N CharPlyMat R )
cayleyhamilton.k 
|- K = ( coe1 ` ( C ` M ) )
cayleyhamilton.m 
|- .* = ( .s ` A )
cayleyhamilton.e 
|- .^ = ( .g ` ( mulGrp ` A ) )
Assertion cayleyhamilton 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )

Proof

Step Hyp Ref Expression
1 cayleyhamilton.a 
 |-  A = ( N Mat R )
2 cayleyhamilton.b 
 |-  B = ( Base ` A )
3 cayleyhamilton.0 
 |-  .0. = ( 0g ` A )
4 cayleyhamilton.c 
 |-  C = ( N CharPlyMat R )
5 cayleyhamilton.k 
 |-  K = ( coe1 ` ( C ` M ) )
6 cayleyhamilton.m 
 |-  .* = ( .s ` A )
7 cayleyhamilton.e 
 |-  .^ = ( .g ` ( mulGrp ` A ) )
8 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
9 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
10 eqid 
 |-  ( N Mat ( Poly1 ` R ) ) = ( N Mat ( Poly1 ` R ) )
11 eqid 
 |-  ( .r ` ( N Mat ( Poly1 ` R ) ) ) = ( .r ` ( N Mat ( Poly1 ` R ) ) )
12 eqid 
 |-  ( -g ` ( N Mat ( Poly1 ` R ) ) ) = ( -g ` ( N Mat ( Poly1 ` R ) ) )
13 eqid 
 |-  ( 0g ` ( N Mat ( Poly1 ` R ) ) ) = ( 0g ` ( N Mat ( Poly1 ` R ) ) )
14 eqid 
 |-  ( Base ` ( N Mat ( Poly1 ` R ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) )
15 eqid 
 |-  ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) ) = ( .g ` ( mulGrp ` ( N Mat ( Poly1 ` R ) ) ) )
16 eqid 
 |-  ( N matToPolyMat R ) = ( N matToPolyMat R )
17 eqeq1 
 |-  ( l = n -> ( l = 0 <-> n = 0 ) )
18 eqeq1 
 |-  ( l = n -> ( l = ( x + 1 ) <-> n = ( x + 1 ) ) )
19 breq2 
 |-  ( l = n -> ( ( x + 1 ) < l <-> ( x + 1 ) < n ) )
20 fvoveq1 
 |-  ( l = n -> ( y ` ( l - 1 ) ) = ( y ` ( n - 1 ) ) )
21 20 fveq2d 
 |-  ( l = n -> ( ( N matToPolyMat R ) ` ( y ` ( l - 1 ) ) ) = ( ( N matToPolyMat R ) ` ( y ` ( n - 1 ) ) ) )
22 2fveq3 
 |-  ( l = n -> ( ( N matToPolyMat R ) ` ( y ` l ) ) = ( ( N matToPolyMat R ) ` ( y ` n ) ) )
23 22 oveq2d 
 |-  ( l = n -> ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` l ) ) ) = ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` n ) ) ) )
24 21 23 oveq12d 
 |-  ( l = n -> ( ( ( N matToPolyMat R ) ` ( y ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` l ) ) ) ) = ( ( ( N matToPolyMat R ) ` ( y ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` n ) ) ) ) )
25 19 24 ifbieq2d 
 |-  ( l = n -> if ( ( x + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( y ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` l ) ) ) ) ) = if ( ( x + 1 ) < n , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( y ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` n ) ) ) ) ) )
26 18 25 ifbieq2d 
 |-  ( l = n -> if ( l = ( x + 1 ) , ( ( N matToPolyMat R ) ` ( y ` x ) ) , if ( ( x + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( y ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` l ) ) ) ) ) ) = if ( n = ( x + 1 ) , ( ( N matToPolyMat R ) ` ( y ` x ) ) , if ( ( x + 1 ) < n , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( y ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` n ) ) ) ) ) ) )
27 17 26 ifbieq2d 
 |-  ( l = n -> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` 0 ) ) ) ) , if ( l = ( x + 1 ) , ( ( N matToPolyMat R ) ` ( y ` x ) ) , if ( ( x + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( y ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` l ) ) ) ) ) ) ) = if ( n = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` 0 ) ) ) ) , if ( n = ( x + 1 ) , ( ( N matToPolyMat R ) ` ( y ` x ) ) , if ( ( x + 1 ) < n , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( y ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` n ) ) ) ) ) ) ) )
28 27 cbvmptv 
 |-  ( l e. NN0 |-> if ( l = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` 0 ) ) ) ) , if ( l = ( x + 1 ) , ( ( N matToPolyMat R ) ` ( y ` x ) ) , if ( ( x + 1 ) < l , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( y ` ( l - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` l ) ) ) ) ) ) ) ) = ( n e. NN0 |-> if ( n = 0 , ( ( 0g ` ( N Mat ( Poly1 ` R ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` 0 ) ) ) ) , if ( n = ( x + 1 ) , ( ( N matToPolyMat R ) ` ( y ` x ) ) , if ( ( x + 1 ) < n , ( 0g ` ( N Mat ( Poly1 ` R ) ) ) , ( ( ( N matToPolyMat R ) ` ( y ` ( n - 1 ) ) ) ( -g ` ( N Mat ( Poly1 ` R ) ) ) ( ( ( N matToPolyMat R ) ` M ) ( .r ` ( N Mat ( Poly1 ` R ) ) ) ( ( N matToPolyMat R ) ` ( y ` n ) ) ) ) ) ) ) )
29 eqid 
 |-  ( N cPolyMatToMat R ) = ( N cPolyMatToMat R )
30 1 2 3 8 6 7 4 5 9 10 11 12 13 14 15 16 28 29 cayleyhamilton0 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )