Metamath Proof Explorer

Theorem chpscmatgsummon

Description: The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of scaled monomials. (Contributed by AV, 2-Sep-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 )
chpscmatgsum.f 
|- F = ( .g ` P )
chpscmatgsum.h 
|- H = ( mulGrp ` R )
chpscmatgsum.e 
|- E = ( .g ` H )
chpscmatgsum.i 
|- I = ( invg ` R )
chpscmatgsum.s 
|- .x. = ( .s ` P )
chpscmatgsum.z 
|- Z = ( .g ` R )
Assertion chpscmatgsummon 
|- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( C ` M ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( ( # ` N ) _C l ) Z ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) ) ) )

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 chpscmatgsum.f 
 |-  F = ( .g ` P )
11 chpscmatgsum.h 
 |-  H = ( mulGrp ` R )
12 chpscmatgsum.e 
 |-  E = ( .g ` H )
13 chpscmatgsum.i 
 |-  I = ( invg ` R )
14 chpscmatgsum.s 
 |-  .x. = ( .s ` P )
15 chpscmatgsum.z 
 |-  Z = ( .g ` R )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 chpscmatgsumbin 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( C ` M ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) ) ) )
17 crngring 
 |-  ( R e. CRing -> R e. Ring )
18 17 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
19 2 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
20 18 19 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. LMod )
21 20 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> P e. LMod )
22 eqid 
 |-  ( Base ` R ) = ( Base ` R )
23 11 22 mgpbas 
 |-  ( Base ` R ) = ( Base ` H )
24 11 ringmgp 
 |-  ( R e. Ring -> H e. Mnd )
25 18 24 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> H e. Mnd )
26 25 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> H e. Mnd )
27 fznn0sub 
 |-  ( l e. ( 0 ... ( # ` N ) ) -> ( ( # ` N ) - l ) e. NN0 )
28 27 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( # ` N ) - l ) e. NN0 )
29 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
30 17 29 syl 
 |-  ( R e. CRing -> R e. Grp )
31 30 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Grp )
32 simp2 
 |-  ( ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) -> J e. N )
33 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 ) )
34 33 7 eleq2s 
 |-  ( M e. D -> M e. ( Base ` A ) )
35 34 3ad2ant1 
 |-  ( ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) -> M e. ( Base ` A ) )
36 32 32 35 3jca 
 |-  ( ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) -> ( J e. N /\ J e. N /\ M e. ( Base ` A ) ) )
37 36 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( J e. N /\ J e. N /\ M e. ( Base ` A ) ) )
38 3 22 matecl 
 |-  ( ( J e. N /\ J e. N /\ M e. ( Base ` A ) ) -> ( J M J ) e. ( Base ` R ) )
39 37 38 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( J M J ) e. ( Base ` R ) )
40 22 13 grpinvcl 
 |-  ( ( R e. Grp /\ ( J M J ) e. ( Base ` R ) ) -> ( I ` ( J M J ) ) e. ( Base ` R ) )
41 31 39 40 syl2an2r 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( I ` ( J M J ) ) e. ( Base ` R ) )
42 41 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( I ` ( J M J ) ) e. ( Base ` R ) )
43 23 12 26 28 42 mulgnn0cld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) e. ( Base ` R ) )
44 2 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
45 44 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` P ) )
46 45 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Scalar ` P ) = R )
47 46 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
48 47 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
49 43 48 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) e. ( Base ` ( Scalar ` P ) ) )
50 hashcl 
 |-  ( N e. Fin -> ( # ` N ) e. NN0 )
51 50 ad2antrr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( # ` N ) e. NN0 )
52 elfzelz 
 |-  ( l e. ( 0 ... ( # ` N ) ) -> l e. ZZ )
53 bccl 
 |-  ( ( ( # ` N ) e. NN0 /\ l e. ZZ ) -> ( ( # ` N ) _C l ) e. NN0 )
54 51 52 53 syl2an 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( # ` N ) _C l ) e. NN0 )
55 eqid 
 |-  ( Base ` P ) = ( Base ` P )
56 5 55 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
57 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
58 5 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
59 17 57 58 3syl 
 |-  ( R e. CRing -> G e. Mnd )
60 59 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> G e. Mnd )
61 60 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> G e. Mnd )
62 elfznn0 
 |-  ( l e. ( 0 ... ( # ` N ) ) -> l e. NN0 )
63 62 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> l e. NN0 )
64 4 2 55 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
65 18 64 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` P ) )
66 65 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> X e. ( Base ` P ) )
67 56 6 61 63 66 mulgnn0cld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( l .^ X ) e. ( Base ` P ) )
68 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
69 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
70 eqid 
 |-  ( .g ` ( Scalar ` P ) ) = ( .g ` ( Scalar ` P ) )
71 55 68 14 69 10 70 lmodvsmmulgdi 
 |-  ( ( P e. LMod /\ ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) e. ( Base ` ( Scalar ` P ) ) /\ ( ( # ` N ) _C l ) e. NN0 /\ ( l .^ X ) e. ( Base ` P ) ) ) -> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) = ( ( ( ( # ` N ) _C l ) ( .g ` ( Scalar ` P ) ) ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) )
72 21 49 54 67 71 syl13anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) = ( ( ( ( # ` N ) _C l ) ( .g ` ( Scalar ` P ) ) ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) )
73 45 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( .g ` R ) = ( .g ` ( Scalar ` P ) ) )
74 15 73 eqtr2id 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( .g ` ( Scalar ` P ) ) = Z )
75 74 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( .g ` ( Scalar ` P ) ) = Z )
76 75 oveqd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( # ` N ) _C l ) ( .g ` ( Scalar ` P ) ) ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) = ( ( ( # ` N ) _C l ) Z ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) )
77 76 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( ( # ` N ) _C l ) ( .g ` ( Scalar ` P ) ) ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) = ( ( ( ( # ` N ) _C l ) Z ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) )
78 72 77 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) /\ l e. ( 0 ... ( # ` N ) ) ) -> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) = ( ( ( ( # ` N ) _C l ) Z ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) )
79 78 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) ) = ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( ( # ` N ) _C l ) Z ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) ) )
80 79 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( # ` N ) _C l ) F ( ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) .x. ( l .^ X ) ) ) ) ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( ( # ` N ) _C l ) Z ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) ) ) )
81 16 80 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) ) -> ( C ` M ) = ( P gsum ( l e. ( 0 ... ( # ` N ) ) |-> ( ( ( ( # ` N ) _C l ) Z ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) ) .x. ( l .^ X ) ) ) ) )