Metamath Proof Explorer

Theorem 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 
|- .0. = ( 0g ` A )
cayleyhamilton0.1 
|- .1. = ( 1r ` A )
cayleyhamilton0.m 
|- .* = ( .s ` A )
cayleyhamilton0.e1 
|- .^ = ( .g ` ( mulGrp ` A ) )
cayleyhamilton0.c 
|- C = ( N CharPlyMat R )
cayleyhamilton0.k 
|- K = ( coe1 ` ( C ` M ) )
cayleyhamilton0.p 
|- P = ( Poly1 ` R )
cayleyhamilton0.y 
|- Y = ( N Mat P )
cayleyhamilton0.r 
|- .X. = ( .r ` Y )
cayleyhamilton0.s 
|- .- = ( -g ` Y )
cayleyhamilton0.z 
|- Z = ( 0g ` Y )
cayleyhamilton0.w 
|- W = ( Base ` Y )
cayleyhamilton0.e2 
|- E = ( .g ` ( mulGrp ` Y ) )
cayleyhamilton0.t 
|- T = ( N matToPolyMat R )
cayleyhamilton0.g 
|- G = ( n e. NN0 |-> if ( n = 0 , ( Z .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , Z , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
cayleyhamilton0.u 
|- U = ( N cPolyMatToMat R )
Assertion cayleyhamilton0 
|- ( ( 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 cayleyhamilton0.a 
 |-  A = ( N Mat R )
2 cayleyhamilton0.b 
 |-  B = ( Base ` A )
3 cayleyhamilton0.0 
 |-  .0. = ( 0g ` A )
4 cayleyhamilton0.1 
 |-  .1. = ( 1r ` A )
5 cayleyhamilton0.m 
 |-  .* = ( .s ` A )
6 cayleyhamilton0.e1 
 |-  .^ = ( .g ` ( mulGrp ` A ) )
7 cayleyhamilton0.c 
 |-  C = ( N CharPlyMat R )
8 cayleyhamilton0.k 
 |-  K = ( coe1 ` ( C ` M ) )
9 cayleyhamilton0.p 
 |-  P = ( Poly1 ` R )
10 cayleyhamilton0.y 
 |-  Y = ( N Mat P )
11 cayleyhamilton0.r 
 |-  .X. = ( .r ` Y )
12 cayleyhamilton0.s 
 |-  .- = ( -g ` Y )
13 cayleyhamilton0.z 
 |-  Z = ( 0g ` Y )
14 cayleyhamilton0.w 
 |-  W = ( Base ` Y )
15 cayleyhamilton0.e2 
 |-  E = ( .g ` ( mulGrp ` Y ) )
16 cayleyhamilton0.t 
 |-  T = ( N matToPolyMat R )
17 cayleyhamilton0.g 
 |-  G = ( n e. NN0 |-> if ( n = 0 , ( Z .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , Z , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( 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 e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) )
21 8 eqcomi 
 |-  ( coe1 ` ( C ` M ) ) = K
22 21 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( coe1 ` ( C ` M ) ) = K )
23 22 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( ( coe1 ` ( C ` M ) ) ` n ) = ( K ` n ) )
24 23 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) = ( ( K ` n ) .* ( n .^ M ) ) )
25 24 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) = ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) )
26 25 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) )
27 26 eqeq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) <-> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) ) )
28 27 biimpa 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) )
29 oveq1 
 |-  ( n = l -> ( n E ( T ` M ) ) = ( l E ( T ` M ) ) )
30 fveq2 
 |-  ( n = l -> ( G ` n ) = ( G ` l ) )
31 29 30 oveq12d 
 |-  ( n = l -> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) = ( ( l E ( T ` M ) ) .X. ( G ` l ) ) )
32 31 cbvmptv 
 |-  ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) = ( l e. NN0 |-> ( ( l E ( T ` M ) ) .X. ( G ` l ) ) )
33 32 oveq2i 
 |-  ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) = ( Y gsum ( l e. NN0 |-> ( ( l E ( T ` M ) ) .X. ( G ` l ) ) ) )
34 1 2 9 10 11 12 13 16 17 15 cayhamlem1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( l e. NN0 |-> ( ( l E ( T ` M ) ) .X. ( G ` l ) ) ) ) = Z )
35 33 34 eqtrid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) = Z )
36 fveq2 
 |-  ( ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) = Z -> ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) = ( U ` Z ) )
37 crngring 
 |-  ( R e. CRing -> R e. Ring )
38 37 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
39 38 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
40 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
41 1 18 9 10 40 13 m2cpminv0 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( U ` Z ) = ( 0g ` A ) )
42 39 41 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( U ` Z ) = ( 0g ` A ) )
43 42 3 eqtr4di 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( U ` Z ) = .0. )
44 43 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( U ` Z ) = .0. )
45 36 44 sylan9eqr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) = Z ) -> ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) = .0. )
46 35 45 mpdan 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) = .0. )
47 46 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) ) -> ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) = .0. )
48 28 47 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )
49 48 ex 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. ) )
50 49 rexlimdvva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` ( C ` M ) ) ` n ) .* ( n .^ M ) ) ) ) = ( U ` ( Y gsum ( n e. NN0 |-> ( ( n E ( T ` M ) ) .X. ( G ` n ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. ) )
51 20 50 mpd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )