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 ˙ = 0 A
cayleyhamilton0.1 1 ˙ = 1 A
cayleyhamilton0.m ˙ = A
cayleyhamilton0.e1 × ˙ = 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 × ˙ = Y
cayleyhamilton0.s - ˙ = - Y
cayleyhamilton0.z Z = 0 Y
cayleyhamilton0.w W = Base Y
cayleyhamilton0.e2 E = mulGrp Y
cayleyhamilton0.t T = N matToPolyMat R
cayleyhamilton0.g G = n 0 if n = 0 Z - ˙ T M × ˙ T b 0 if n = s + 1 T b s if s + 1 < n Z T b n 1 - ˙ T M × ˙ T b n
cayleyhamilton0.u U = N cPolyMatToMat R
Assertion cayleyhamilton0 N Fin R CRing M B A n 0 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 ˙ = 0 A
4 cayleyhamilton0.1 1 ˙ = 1 A
5 cayleyhamilton0.m ˙ = A
6 cayleyhamilton0.e1 × ˙ = 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 × ˙ = Y
12 cayleyhamilton0.s - ˙ = - Y
13 cayleyhamilton0.z Z = 0 Y
14 cayleyhamilton0.w W = Base Y
15 cayleyhamilton0.e2 E = mulGrp Y
16 cayleyhamilton0.t T = N matToPolyMat R
17 cayleyhamilton0.g G = n 0 if n = 0 Z - ˙ T M × ˙ T b 0 if n = s + 1 T b s if s + 1 < n Z T b n 1 - ˙ T M × ˙ 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 Fin R CRing M B s b B 0 s A n 0 coe 1 C M n ˙ n × ˙ M = U Y n 0 n E T M × ˙ G n
21 8 eqcomi coe 1 C M = K
22 21 a1i N Fin R CRing M B s b B 0 s n 0 coe 1 C M = K
23 22 fveq1d N Fin R CRing M B s b B 0 s n 0 coe 1 C M n = K n
24 23 oveq1d N Fin R CRing M B s b B 0 s n 0 coe 1 C M n ˙ n × ˙ M = K n ˙ n × ˙ M
25 24 mpteq2dva N Fin R CRing M B s b B 0 s n 0 coe 1 C M n ˙ n × ˙ M = n 0 K n ˙ n × ˙ M
26 25 oveq2d N Fin R CRing M B s b B 0 s A n 0 coe 1 C M n ˙ n × ˙ M = A n 0 K n ˙ n × ˙ M
27 26 eqeq1d N Fin R CRing M B s b B 0 s A n 0 coe 1 C M n ˙ n × ˙ M = U Y n 0 n E T M × ˙ G n A n 0 K n ˙ n × ˙ M = U Y n 0 n E T M × ˙ G n
28 27 biimpa N Fin R CRing M B s b B 0 s A n 0 coe 1 C M n ˙ n × ˙ M = U Y n 0 n E T M × ˙ G n A n 0 K n ˙ n × ˙ M = U Y n 0 n E T M × ˙ 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 × ˙ G n = l E T M × ˙ G l
32 31 cbvmptv n 0 n E T M × ˙ G n = l 0 l E T M × ˙ G l
33 32 oveq2i Y n 0 n E T M × ˙ G n = Y l 0 l E T M × ˙ G l
34 1 2 9 10 11 12 13 16 17 15 cayhamlem1 N Fin R CRing M B s b B 0 s Y l 0 l E T M × ˙ G l = Z
35 33 34 syl5eq N Fin R CRing M B s b B 0 s Y n 0 n E T M × ˙ G n = Z
36 fveq2 Y n 0 n E T M × ˙ G n = Z U Y n 0 n E T M × ˙ G n = U Z
37 crngring R CRing R Ring
38 37 anim2i N Fin R CRing N Fin R Ring
39 38 3adant3 N Fin R CRing M B N Fin R Ring
40 eqid 0 A = 0 A
41 1 18 9 10 40 13 m2cpminv0 N Fin R Ring U Z = 0 A
42 39 41 syl N Fin R CRing M B U Z = 0 A
43 42 3 eqtr4di N Fin R CRing M B U Z = 0 ˙
44 43 adantr N Fin R CRing M B s b B 0 s U Z = 0 ˙
45 36 44 sylan9eqr N Fin R CRing M B s b B 0 s Y n 0 n E T M × ˙ G n = Z U Y n 0 n E T M × ˙ G n = 0 ˙
46 35 45 mpdan N Fin R CRing M B s b B 0 s U Y n 0 n E T M × ˙ G n = 0 ˙
47 46 adantr N Fin R CRing M B s b B 0 s A n 0 coe 1 C M n ˙ n × ˙ M = U Y n 0 n E T M × ˙ G n U Y n 0 n E T M × ˙ G n = 0 ˙
48 28 47 eqtrd N Fin R CRing M B s b B 0 s A n 0 coe 1 C M n ˙ n × ˙ M = U Y n 0 n E T M × ˙ G n A n 0 K n ˙ n × ˙ M = 0 ˙
49 48 ex N Fin R CRing M B s b B 0 s A n 0 coe 1 C M n ˙ n × ˙ M = U Y n 0 n E T M × ˙ G n A n 0 K n ˙ n × ˙ M = 0 ˙
50 49 rexlimdvva N Fin R CRing M B s b B 0 s A n 0 coe 1 C M n ˙ n × ˙ M = U Y n 0 n E T M × ˙ G n A n 0 K n ˙ n × ˙ M = 0 ˙
51 20 50 mpd N Fin R CRing M B A n 0 K n ˙ n × ˙ M = 0 ˙