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 ffvelrnd
 |-  ( ( ( 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 ) ) ) )