Metamath Proof Explorer

Theorem chpscmat

Description: The characteristic polynomial of a (nonempty!) scalar matrix. (Contributed by AV, 21-Aug-2019)

Ref Expression
Hypotheses chp0mat.c 
|- C = ( N CharPlyMat R )
chp0mat.p 
|- P = ( Poly1 ` R )
chp0mat.a 
|- A = ( N Mat R )
chp0mat.x 
|- X = ( var1 ` R )
chp0mat.g 
|- G = ( mulGrp ` P )
chp0mat.m 
|- .^ = ( .g ` G )
chpscmat.d 
|- D = { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) }
chpscmat.s 
|- S = ( algSc ` P )
chpscmat.m 
|- .- = ( -g ` P )
Assertion chpscmat 
|- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( C ` M ) = ( ( # ` N ) .^ ( X .- ( S ` E ) ) ) )

Proof

Step Hyp Ref Expression
1 chp0mat.c 
 |-  C = ( N CharPlyMat R )
2 chp0mat.p 
 |-  P = ( Poly1 ` R )
3 chp0mat.a 
 |-  A = ( N Mat R )
4 chp0mat.x 
 |-  X = ( var1 ` R )
5 chp0mat.g 
 |-  G = ( mulGrp ` P )
6 chp0mat.m 
 |-  .^ = ( .g ` G )
7 chpscmat.d 
 |-  D = { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) }
8 chpscmat.s 
 |-  S = ( algSc ` P )
9 chpscmat.m 
 |-  .- = ( -g ` P )
10 simpll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> N e. Fin )
11 simplr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> R e. CRing )
12 elrabi 
 |-  ( M e. { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) } -> M e. ( Base ` A ) )
13 12 7 eleq2s 
 |-  ( M e. D -> M e. ( Base ` A ) )
14 13 3ad2ant1 
 |-  ( ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) -> M e. ( Base ` A ) )
15 14 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> M e. ( Base ` A ) )
16 oveq 
 |-  ( m = M -> ( i m j ) = ( i M j ) )
17 16 eqeq1d 
 |-  ( m = M -> ( ( i m j ) = if ( i = j , c , ( 0g ` R ) ) <-> ( i M j ) = if ( i = j , c , ( 0g ` R ) ) ) )
18 17 2ralbidv 
 |-  ( m = M -> ( A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) <-> A. i e. N A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) ) )
19 18 rexbidv 
 |-  ( m = M -> ( E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) <-> E. c e. ( Base ` R ) A. i e. N A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) ) )
20 19 elrab 
 |-  ( M e. { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) } <-> ( M e. ( Base ` A ) /\ E. c e. ( Base ` R ) A. i e. N A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) ) )
21 ifnefalse 
 |-  ( i =/= j -> if ( i = j , c , ( 0g ` R ) ) = ( 0g ` R ) )
22 21 eqeq2d 
 |-  ( i =/= j -> ( ( i M j ) = if ( i = j , c , ( 0g ` R ) ) <-> ( i M j ) = ( 0g ` R ) ) )
23 22 biimpcd 
 |-  ( ( i M j ) = if ( i = j , c , ( 0g ` R ) ) -> ( i =/= j -> ( i M j ) = ( 0g ` R ) ) )
24 23 a1i 
 |-  ( ( ( ( ( M e. ( Base ` A ) /\ c e. ( Base ` R ) ) /\ ( N e. Fin /\ R e. CRing ) ) /\ i e. N ) /\ j e. N ) -> ( ( i M j ) = if ( i = j , c , ( 0g ` R ) ) -> ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) )
25 24 ralimdva 
 |-  ( ( ( ( M e. ( Base ` A ) /\ c e. ( Base ` R ) ) /\ ( N e. Fin /\ R e. CRing ) ) /\ i e. N ) -> ( A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) -> A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) )
26 25 ralimdva 
 |-  ( ( ( M e. ( Base ` A ) /\ c e. ( Base ` R ) ) /\ ( N e. Fin /\ R e. CRing ) ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) )
27 26 ex 
 |-  ( ( M e. ( Base ` A ) /\ c e. ( Base ` R ) ) -> ( ( N e. Fin /\ R e. CRing ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) ) )
28 27 com23 
 |-  ( ( M e. ( Base ` A ) /\ c e. ( Base ` R ) ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) -> ( ( N e. Fin /\ R e. CRing ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) ) )
29 28 rexlimdva 
 |-  ( M e. ( Base ` A ) -> ( E. c e. ( Base ` R ) A. i e. N A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) -> ( ( N e. Fin /\ R e. CRing ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) ) )
30 29 imp 
 |-  ( ( M e. ( Base ` A ) /\ E. c e. ( Base ` R ) A. i e. N A. j e. N ( i M j ) = if ( i = j , c , ( 0g ` R ) ) ) -> ( ( N e. Fin /\ R e. CRing ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) )
31 20 30 sylbi 
 |-  ( M e. { m e. ( Base ` A ) | E. c e. ( Base ` R ) A. i e. N A. j e. N ( i m j ) = if ( i = j , c , ( 0g ` R ) ) } -> ( ( N e. Fin /\ R e. CRing ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) )
32 31 7 eleq2s 
 |-  ( M e. D -> ( ( N e. Fin /\ R e. CRing ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) )
33 32 3ad2ant1 
 |-  ( ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) -> ( ( N e. Fin /\ R e. CRing ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) )
34 33 impcom 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) )
35 eqid 
 |-  ( Base ` A ) = ( Base ` A )
36 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
37 1 2 3 8 35 4 36 5 9 chpdmat 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. ( Base ` A ) ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = ( 0g ` R ) ) ) -> ( C ` M ) = ( G gsum ( k e. N |-> ( X .- ( S ` ( k M k ) ) ) ) ) )
38 10 11 15 34 37 syl31anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( C ` M ) = ( G gsum ( k e. N |-> ( X .- ( S ` ( k M k ) ) ) ) ) )
39 id 
 |-  ( n = k -> n = k )
40 39 39 oveq12d 
 |-  ( n = k -> ( n M n ) = ( k M k ) )
41 40 eqeq1d 
 |-  ( n = k -> ( ( n M n ) = E <-> ( k M k ) = E ) )
42 41 rspccv 
 |-  ( A. n e. N ( n M n ) = E -> ( k e. N -> ( k M k ) = E ) )
43 42 3ad2ant3 
 |-  ( ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) -> ( k e. N -> ( k M k ) = E ) )
44 43 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( k e. N -> ( k M k ) = E ) )
45 44 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) /\ k e. N ) -> ( k M k ) = E )
46 45 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) /\ k e. N ) -> ( S ` ( k M k ) ) = ( S ` E ) )
47 46 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) /\ k e. N ) -> ( X .- ( S ` ( k M k ) ) ) = ( X .- ( S ` E ) ) )
48 47 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( k e. N |-> ( X .- ( S ` ( k M k ) ) ) ) = ( k e. N |-> ( X .- ( S ` E ) ) ) )
49 48 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( G gsum ( k e. N |-> ( X .- ( S ` ( k M k ) ) ) ) ) = ( G gsum ( k e. N |-> ( X .- ( S ` E ) ) ) ) )
50 2 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
51 5 crngmgp 
 |-  ( P e. CRing -> G e. CMnd )
52 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
53 50 51 52 3syl 
 |-  ( R e. CRing -> G e. Mnd )
54 53 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> G e. Mnd )
55 crngring 
 |-  ( R e. CRing -> R e. Ring )
56 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
57 55 56 syl 
 |-  ( R e. CRing -> P e. Ring )
58 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
59 57 58 syl 
 |-  ( R e. CRing -> P e. Grp )
60 59 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> P e. Grp )
61 eqid 
 |-  ( Base ` P ) = ( Base ` P )
62 4 2 61 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
63 55 62 syl 
 |-  ( R e. CRing -> X e. ( Base ` P ) )
64 63 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> X e. ( Base ` P ) )
65 simpr 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> I e. N )
66 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
67 57 ad2antll 
 |-  ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) -> P e. Ring )
68 67 adantr 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> P e. Ring )
69 2 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
70 55 69 syl 
 |-  ( R e. CRing -> P e. LMod )
71 70 ad2antll 
 |-  ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) -> P e. LMod )
72 71 adantr 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> P e. LMod )
73 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
74 8 66 68 72 73 61 asclf 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> S : ( Base ` ( Scalar ` P ) ) --> ( Base ` P ) )
75 13 adantr 
 |-  ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) -> M e. ( Base ` A ) )
76 75 adantr 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> M e. ( Base ` A ) )
77 eqid 
 |-  ( Base ` R ) = ( Base ` R )
78 3 77 matecl 
 |-  ( ( I e. N /\ I e. N /\ M e. ( Base ` A ) ) -> ( I M I ) e. ( Base ` R ) )
79 65 65 76 78 syl3anc 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> ( I M I ) e. ( Base ` R ) )
80 2 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
81 80 ad2antll 
 |-  ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) -> R = ( Scalar ` P ) )
82 81 adantr 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> R = ( Scalar ` P ) )
83 82 eqcomd 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> ( Scalar ` P ) = R )
84 83 fveq2d 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
85 79 84 eleqtrrd 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> ( I M I ) e. ( Base ` ( Scalar ` P ) ) )
86 74 85 ffvelcdmd 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> ( S ` ( I M I ) ) e. ( Base ` P ) )
87 fveq2 
 |-  ( E = ( I M I ) -> ( S ` E ) = ( S ` ( I M I ) ) )
88 87 eqcoms 
 |-  ( ( I M I ) = E -> ( S ` E ) = ( S ` ( I M I ) ) )
89 88 eleq1d 
 |-  ( ( I M I ) = E -> ( ( S ` E ) e. ( Base ` P ) <-> ( S ` ( I M I ) ) e. ( Base ` P ) ) )
90 86 89 syl5ibrcom 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> ( ( I M I ) = E -> ( S ` E ) e. ( Base ` P ) ) )
91 90 adantr 
 |-  ( ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) /\ n = I ) -> ( ( I M I ) = E -> ( S ` E ) e. ( Base ` P ) ) )
92 id 
 |-  ( n = I -> n = I )
93 92 92 oveq12d 
 |-  ( n = I -> ( n M n ) = ( I M I ) )
94 93 eqeq1d 
 |-  ( n = I -> ( ( n M n ) = E <-> ( I M I ) = E ) )
95 94 imbi1d 
 |-  ( n = I -> ( ( ( n M n ) = E -> ( S ` E ) e. ( Base ` P ) ) <-> ( ( I M I ) = E -> ( S ` E ) e. ( Base ` P ) ) ) )
96 95 adantl 
 |-  ( ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) /\ n = I ) -> ( ( ( n M n ) = E -> ( S ` E ) e. ( Base ` P ) ) <-> ( ( I M I ) = E -> ( S ` E ) e. ( Base ` P ) ) ) )
97 91 96 mpbird 
 |-  ( ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) /\ n = I ) -> ( ( n M n ) = E -> ( S ` E ) e. ( Base ` P ) ) )
98 65 97 rspcimdv 
 |-  ( ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) /\ I e. N ) -> ( A. n e. N ( n M n ) = E -> ( S ` E ) e. ( Base ` P ) ) )
99 98 ex 
 |-  ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) -> ( I e. N -> ( A. n e. N ( n M n ) = E -> ( S ` E ) e. ( Base ` P ) ) ) )
100 99 com23 
 |-  ( ( M e. D /\ ( N e. Fin /\ R e. CRing ) ) -> ( A. n e. N ( n M n ) = E -> ( I e. N -> ( S ` E ) e. ( Base ` P ) ) ) )
101 100 ex 
 |-  ( M e. D -> ( ( N e. Fin /\ R e. CRing ) -> ( A. n e. N ( n M n ) = E -> ( I e. N -> ( S ` E ) e. ( Base ` P ) ) ) ) )
102 101 com24 
 |-  ( M e. D -> ( I e. N -> ( A. n e. N ( n M n ) = E -> ( ( N e. Fin /\ R e. CRing ) -> ( S ` E ) e. ( Base ` P ) ) ) ) )
103 102 3imp 
 |-  ( ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) -> ( ( N e. Fin /\ R e. CRing ) -> ( S ` E ) e. ( Base ` P ) ) )
104 103 impcom 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( S ` E ) e. ( Base ` P ) )
105 61 9 grpsubcl 
 |-  ( ( P e. Grp /\ X e. ( Base ` P ) /\ ( S ` E ) e. ( Base ` P ) ) -> ( X .- ( S ` E ) ) e. ( Base ` P ) )
106 60 64 104 105 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( X .- ( S ` E ) ) e. ( Base ` P ) )
107 5 61 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
108 106 107 eleqtrdi 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( X .- ( S ` E ) ) e. ( Base ` G ) )
109 eqid 
 |-  ( Base ` G ) = ( Base ` G )
110 109 6 gsumconst 
 |-  ( ( G e. Mnd /\ N e. Fin /\ ( X .- ( S ` E ) ) e. ( Base ` G ) ) -> ( G gsum ( k e. N |-> ( X .- ( S ` E ) ) ) ) = ( ( # ` N ) .^ ( X .- ( S ` E ) ) ) )
111 54 10 108 110 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( G gsum ( k e. N |-> ( X .- ( S ` E ) ) ) ) = ( ( # ` N ) .^ ( X .- ( S ` E ) ) ) )
112 38 49 111 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ I e. N /\ A. n e. N ( n M n ) = E ) ) -> ( C ` M ) = ( ( # ` N ) .^ ( X .- ( S ` E ) ) ) )