Metamath Proof Explorer

Theorem cayleyhamilton1

Description: The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", or, in other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. In this variant of cayleyhamilton , the meaning of "inserted" is made more transparent: If the characteristic polynomial is a polynomial with coefficients ( Fn ) , then a matrix over a commutative ring "inserted" into its characteristic polynomial is the sum of these coefficients multiplied with the corresponding power of the matrix. (Contributed by AV, 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 ) )
cayleyhamilton1.l 
|- L = ( Base ` R )
cayleyhamilton1.x 
|- X = ( var1 ` R )
cayleyhamilton1.p 
|- P = ( Poly1 ` R )
cayleyhamilton1.m 
|- .x. = ( .s ` P )
cayleyhamilton1.e 
|- E = ( .g ` ( mulGrp ` P ) )
cayleyhamilton1.z 
|- Z = ( 0g ` R )
Assertion cayleyhamilton1 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( F ` 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 cayleyhamilton1.l 
 |-  L = ( Base ` R )
9 cayleyhamilton1.x 
 |-  X = ( var1 ` R )
10 cayleyhamilton1.p 
 |-  P = ( Poly1 ` R )
11 cayleyhamilton1.m 
 |-  .x. = ( .s ` P )
12 cayleyhamilton1.e 
 |-  E = ( .g ` ( mulGrp ` P ) )
13 cayleyhamilton1.z 
 |-  Z = ( 0g ` R )
14 1 2 3 4 5 6 7 cayleyhamilton 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )
15 14 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. )
16 nfv 
 |-  F/ n ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) )
17 nfcv 
 |-  F/_ n P
18 nfcv 
 |-  F/_ n gsum
19 nfmpt1 
 |-  F/_ n ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) )
20 17 18 19 nfov 
 |-  F/_ n ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) )
21 20 nfeq2 
 |-  F/ n ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) )
22 16 21 nfan 
 |-  F/ n ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) /\ ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) )
23 crngring 
 |-  ( R e. CRing -> R e. Ring )
24 23 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
25 24 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> R e. Ring )
26 eqid 
 |-  ( Base ` P ) = ( Base ` P )
27 4 1 2 10 26 chpmatply1 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) e. ( Base ` P ) )
28 27 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( C ` M ) e. ( Base ` P ) )
29 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
30 elmapi 
 |-  ( F e. ( L ^m NN0 ) -> F : NN0 --> L )
31 ffvelrn 
 |-  ( ( F : NN0 --> L /\ n e. NN0 ) -> ( F ` n ) e. L )
32 31 ralrimiva 
 |-  ( F : NN0 --> L -> A. n e. NN0 ( F ` n ) e. L )
33 30 32 syl 
 |-  ( F e. ( L ^m NN0 ) -> A. n e. NN0 ( F ` n ) e. L )
34 33 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> A. n e. NN0 ( F ` n ) e. L )
35 30 feqmptd 
 |-  ( F e. ( L ^m NN0 ) -> F = ( n e. NN0 |-> ( F ` n ) ) )
36 13 a1i 
 |-  ( F e. ( L ^m NN0 ) -> Z = ( 0g ` R ) )
37 35 36 breq12d 
 |-  ( F e. ( L ^m NN0 ) -> ( F finSupp Z <-> ( n e. NN0 |-> ( F ` n ) ) finSupp ( 0g ` R ) ) )
38 37 biimpa 
 |-  ( ( F e. ( L ^m NN0 ) /\ F finSupp Z ) -> ( n e. NN0 |-> ( F ` n ) ) finSupp ( 0g ` R ) )
39 38 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( n e. NN0 |-> ( F ` n ) ) finSupp ( 0g ` R ) )
40 10 26 9 12 25 8 11 29 34 39 gsumsmonply1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) e. ( Base ` P ) )
41 fveq2 
 |-  ( i = n -> ( F ` i ) = ( F ` n ) )
42 oveq1 
 |-  ( i = n -> ( i E X ) = ( n E X ) )
43 41 42 oveq12d 
 |-  ( i = n -> ( ( F ` i ) .x. ( i E X ) ) = ( ( F ` n ) .x. ( n E X ) ) )
44 43 cbvmptv 
 |-  ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) = ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) )
45 44 oveq2i 
 |-  ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) )
46 45 fveq2i 
 |-  ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) = ( coe1 ` ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) )
47 10 26 5 46 ply1coe1eq 
 |-  ( ( R e. Ring /\ ( C ` M ) e. ( Base ` P ) /\ ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) e. ( Base ` P ) ) -> ( A. m e. NN0 ( K ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) <-> ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) ) )
48 25 28 40 47 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( A. m e. NN0 ( K ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) <-> ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) ) )
49 fveq2 
 |-  ( m = n -> ( K ` m ) = ( K ` n ) )
50 fveq2 
 |-  ( m = n -> ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) )
51 49 50 eqeq12d 
 |-  ( m = n -> ( ( K ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) <-> ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) ) )
52 51 rspcva 
 |-  ( ( n e. NN0 /\ A. m e. NN0 ( K ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) ) -> ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) )
53 simpl 
 |-  ( ( ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) /\ ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) ) -> ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) )
54 24 ad2antrl 
 |-  ( ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) -> R e. Ring )
55 ffvelrn 
 |-  ( ( F : NN0 --> L /\ i e. NN0 ) -> ( F ` i ) e. L )
56 55 ralrimiva 
 |-  ( F : NN0 --> L -> A. i e. NN0 ( F ` i ) e. L )
57 30 56 syl 
 |-  ( F e. ( L ^m NN0 ) -> A. i e. NN0 ( F ` i ) e. L )
58 57 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> A. i e. NN0 ( F ` i ) e. L )
59 58 adantl 
 |-  ( ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) -> A. i e. NN0 ( F ` i ) e. L )
60 30 feqmptd 
 |-  ( F e. ( L ^m NN0 ) -> F = ( i e. NN0 |-> ( F ` i ) ) )
61 60 breq1d 
 |-  ( F e. ( L ^m NN0 ) -> ( F finSupp Z <-> ( i e. NN0 |-> ( F ` i ) ) finSupp Z ) )
62 61 biimpa 
 |-  ( ( F e. ( L ^m NN0 ) /\ F finSupp Z ) -> ( i e. NN0 |-> ( F ` i ) ) finSupp Z )
63 62 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( i e. NN0 |-> ( F ` i ) ) finSupp Z )
64 63 adantl 
 |-  ( ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) -> ( i e. NN0 |-> ( F ` i ) ) finSupp Z )
65 simpl 
 |-  ( ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) -> n e. NN0 )
66 10 26 9 12 54 8 11 13 59 64 65 gsummoncoe1 
 |-  ( ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) -> ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) = [_ n / i ]_ ( F ` i ) )
67 csbfv 
 |-  [_ n / i ]_ ( F ` i ) = ( F ` n )
68 66 67 eqtrdi 
 |-  ( ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) -> ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) = ( F ` n ) )
69 68 adantl 
 |-  ( ( ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) /\ ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) ) -> ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) = ( F ` n ) )
70 53 69 eqtrd 
 |-  ( ( ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) /\ ( n e. NN0 /\ ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) ) ) -> ( K ` n ) = ( F ` n ) )
71 70 exp32 
 |-  ( ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) -> ( n e. NN0 -> ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( K ` n ) = ( F ` n ) ) ) )
72 71 com12 
 |-  ( n e. NN0 -> ( ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) -> ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( K ` n ) = ( F ` n ) ) ) )
73 72 adantr 
 |-  ( ( n e. NN0 /\ A. m e. NN0 ( K ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) ) -> ( ( K ` n ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` n ) -> ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( K ` n ) = ( F ` n ) ) ) )
74 52 73 mpd 
 |-  ( ( n e. NN0 /\ A. m e. NN0 ( K ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) ) -> ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( K ` n ) = ( F ` n ) ) )
75 74 com12 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( ( n e. NN0 /\ A. m e. NN0 ( K ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) ) -> ( K ` n ) = ( F ` n ) ) )
76 75 expcomd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( A. m e. NN0 ( K ` m ) = ( ( coe1 ` ( P gsum ( i e. NN0 |-> ( ( F ` i ) .x. ( i E X ) ) ) ) ) ` m ) -> ( n e. NN0 -> ( K ` n ) = ( F ` n ) ) ) )
77 48 76 sylbird 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) -> ( n e. NN0 -> ( K ` n ) = ( F ` n ) ) ) )
78 77 imp31 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) /\ ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) ) /\ n e. NN0 ) -> ( K ` n ) = ( F ` n ) )
79 78 oveq1d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) /\ ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) ) /\ n e. NN0 ) -> ( ( K ` n ) .* ( n .^ M ) ) = ( ( F ` n ) .* ( n .^ M ) ) )
80 22 79 mpteq2da 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) /\ ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) ) -> ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) = ( n e. NN0 |-> ( ( F ` n ) .* ( n .^ M ) ) ) )
81 80 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) /\ ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( F ` n ) .* ( n .^ M ) ) ) ) )
82 81 eqeq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) /\ ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) ) -> ( ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. <-> ( A gsum ( n e. NN0 |-> ( ( F ` n ) .* ( n .^ M ) ) ) ) = .0. ) )
83 82 biimpd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) /\ ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) ) -> ( ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. -> ( A gsum ( n e. NN0 |-> ( ( F ` n ) .* ( n .^ M ) ) ) ) = .0. ) )
84 83 ex 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) -> ( ( A gsum ( n e. NN0 |-> ( ( K ` n ) .* ( n .^ M ) ) ) ) = .0. -> ( A gsum ( n e. NN0 |-> ( ( F ` n ) .* ( n .^ M ) ) ) ) = .0. ) ) )
85 15 84 mpid 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( F e. ( L ^m NN0 ) /\ F finSupp Z ) ) -> ( ( C ` M ) = ( P gsum ( n e. NN0 |-> ( ( F ` n ) .x. ( n E X ) ) ) ) -> ( A gsum ( n e. NN0 |-> ( ( F ` n ) .* ( n .^ M ) ) ) ) = .0. ) )