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 11 ringmgp 
 |-  ( R e. Ring -> H e. Mnd )
23 18 22 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> H e. Mnd )
24 23 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 )
25 fznn0sub 
 |-  ( l e. ( 0 ... ( # ` N ) ) -> ( ( # ` N ) - l ) e. NN0 )
26 25 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 )
27 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
28 17 27 syl 
 |-  ( R e. CRing -> R e. Grp )
29 28 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Grp )
30 simp2 
 |-  ( ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) -> J e. N )
31 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 ) )
32 31 7 eleq2s 
 |-  ( M e. D -> M e. ( Base ` A ) )
33 32 3ad2ant1 
 |-  ( ( M e. D /\ J e. N /\ A. n e. N ( n M n ) = ( J M J ) ) -> M e. ( Base ` A ) )
34 30 30 33 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 ) ) )
35 34 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 ) ) )
36 eqid 
 |-  ( Base ` R ) = ( Base ` R )
37 3 36 matecl 
 |-  ( ( J e. N /\ J e. N /\ M e. ( Base ` A ) ) -> ( J M J ) e. ( Base ` R ) )
38 35 37 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 ) )
39 36 13 grpinvcl 
 |-  ( ( R e. Grp /\ ( J M J ) e. ( Base ` R ) ) -> ( I ` ( J M J ) ) e. ( Base ` R ) )
40 29 38 39 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 ) )
41 40 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 ) )
42 11 36 mgpbas 
 |-  ( Base ` R ) = ( Base ` H )
43 42 12 mulgnn0cl 
 |-  ( ( H e. Mnd /\ ( ( # ` N ) - l ) e. NN0 /\ ( I ` ( J M J ) ) e. ( Base ` R ) ) -> ( ( ( # ` N ) - l ) E ( I ` ( J M J ) ) ) e. ( Base ` R ) )
44 24 26 41 43 syl3anc 
 |-  ( ( ( ( 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 ) )
45 2 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
46 45 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` P ) )
47 46 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Scalar ` P ) = R )
48 47 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
49 48 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 ) )
50 44 49 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 ) ) )
51 hashcl 
 |-  ( N e. Fin -> ( # ` N ) e. NN0 )
52 51 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 )
53 elfzelz 
 |-  ( l e. ( 0 ... ( # ` N ) ) -> l e. ZZ )
54 bccl 
 |-  ( ( ( # ` N ) e. NN0 /\ l e. ZZ ) -> ( ( # ` N ) _C l ) e. NN0 )
55 52 53 54 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 )
56 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
57 5 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
58 17 56 57 3syl 
 |-  ( R e. CRing -> G e. Mnd )
59 58 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> G e. Mnd )
60 59 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 )
61 elfznn0 
 |-  ( l e. ( 0 ... ( # ` N ) ) -> l e. NN0 )
62 61 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 )
63 eqid 
 |-  ( Base ` P ) = ( Base ` P )
64 4 2 63 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 5 63 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
68 67 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ l e. NN0 /\ X e. ( Base ` P ) ) -> ( l .^ X ) e. ( Base ` P ) )
69 60 62 66 68 syl3anc 
 |-  ( ( ( ( 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 ) )
70 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
71 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
72 eqid 
 |-  ( .g ` ( Scalar ` P ) ) = ( .g ` ( Scalar ` P ) )
73 63 70 14 71 10 72 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 ) ) )
74 21 50 55 69 73 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 ) ) )
75 46 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( .g ` R ) = ( .g ` ( Scalar ` P ) ) )
76 15 75 eqtr2id 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( .g ` ( Scalar ` P ) ) = Z )
77 76 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 )
78 77 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 ) ) ) ) )
79 78 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 ) ) )
80 74 79 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 ) ) )
81 80 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 ) ) ) )
82 81 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 ) ) ) ) )
83 16 82 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 ) ) ) ) )