Metamath Proof Explorer

Theorem chpidmat

Description: The characteristic polynomial of the identity matrix. (Contributed by AV, 19-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 )
chpidmat.i 
|- I = ( 1r ` A )
chpidmat.s 
|- S = ( algSc ` P )
chpidmat.1 
|- .1. = ( 1r ` R )
chpidmat.m 
|- .- = ( -g ` P )
Assertion chpidmat 
|- ( ( N e. Fin /\ R e. CRing ) -> ( C ` I ) = ( ( # ` N ) .^ ( X .- ( S ` .1. ) ) ) )

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 chpidmat.i 
 |-  I = ( 1r ` A )
8 chpidmat.s 
 |-  S = ( algSc ` P )
9 chpidmat.1 
 |-  .1. = ( 1r ` R )
10 chpidmat.m 
 |-  .- = ( -g ` P )
11 simpl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> N e. Fin )
12 simpr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. CRing )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 3 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
15 13 14 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
16 eqid 
 |-  ( Base ` A ) = ( Base ` A )
17 16 7 ringidcl 
 |-  ( A e. Ring -> I e. ( Base ` A ) )
18 15 17 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> I e. ( Base ` A ) )
19 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
20 11 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> N e. Fin )
21 13 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
22 21 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> R e. Ring )
23 simplrl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> i e. N )
24 simplrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> j e. N )
25 3 9 19 20 22 23 24 7 mat1ov 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i I j ) = if ( i = j , .1. , ( 0g ` R ) ) )
26 ifnefalse 
 |-  ( i =/= j -> if ( i = j , .1. , ( 0g ` R ) ) = ( 0g ` R ) )
27 26 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> if ( i = j , .1. , ( 0g ` R ) ) = ( 0g ` R ) )
28 25 27 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i I j ) = ( 0g ` R ) )
29 28 ex 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) -> ( i =/= j -> ( i I j ) = ( 0g ` R ) ) )
30 29 ralrimivva 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A. i e. N A. j e. N ( i =/= j -> ( i I j ) = ( 0g ` R ) ) )
31 eqid 
 |-  ( -g ` P ) = ( -g ` P )
32 1 2 3 8 16 4 19 5 31 chpdmat 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ I e. ( Base ` A ) ) /\ A. i e. N A. j e. N ( i =/= j -> ( i I j ) = ( 0g ` R ) ) ) -> ( C ` I ) = ( G gsum ( k e. N |-> ( X ( -g ` P ) ( S ` ( k I k ) ) ) ) ) )
33 11 12 18 30 32 syl31anc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( C ` I ) = ( G gsum ( k e. N |-> ( X ( -g ` P ) ( S ` ( k I k ) ) ) ) ) )
34 11 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> N e. Fin )
35 21 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> R e. Ring )
36 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> k e. N )
37 3 9 19 34 35 36 36 7 mat1ov 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( k I k ) = if ( k = k , .1. , ( 0g ` R ) ) )
38 eqid 
 |-  k = k
39 38 iftruei 
 |-  if ( k = k , .1. , ( 0g ` R ) ) = .1.
40 37 39 eqtrdi 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( k I k ) = .1. )
41 40 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( S ` ( k I k ) ) = ( S ` .1. ) )
42 41 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( X ( -g ` P ) ( S ` ( k I k ) ) ) = ( X ( -g ` P ) ( S ` .1. ) ) )
43 42 mpteq2dva 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( k e. N |-> ( X ( -g ` P ) ( S ` ( k I k ) ) ) ) = ( k e. N |-> ( X ( -g ` P ) ( S ` .1. ) ) ) )
44 43 oveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( G gsum ( k e. N |-> ( X ( -g ` P ) ( S ` ( k I k ) ) ) ) ) = ( G gsum ( k e. N |-> ( X ( -g ` P ) ( S ` .1. ) ) ) ) )
45 2 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
46 5 crngmgp 
 |-  ( P e. CRing -> G e. CMnd )
47 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
48 45 46 47 3syl 
 |-  ( R e. CRing -> G e. Mnd )
49 48 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> G e. Mnd )
50 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
51 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
52 50 51 syl 
 |-  ( R e. Ring -> P e. Grp )
53 eqid 
 |-  ( Base ` P ) = ( Base ` P )
54 4 2 53 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
55 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
56 2 8 9 55 ply1scl1 
 |-  ( R e. Ring -> ( S ` .1. ) = ( 1r ` P ) )
57 53 55 ringidcl 
 |-  ( P e. Ring -> ( 1r ` P ) e. ( Base ` P ) )
58 50 57 syl 
 |-  ( R e. Ring -> ( 1r ` P ) e. ( Base ` P ) )
59 56 58 eqeltrd 
 |-  ( R e. Ring -> ( S ` .1. ) e. ( Base ` P ) )
60 52 54 59 3jca 
 |-  ( R e. Ring -> ( P e. Grp /\ X e. ( Base ` P ) /\ ( S ` .1. ) e. ( Base ` P ) ) )
61 13 60 syl 
 |-  ( R e. CRing -> ( P e. Grp /\ X e. ( Base ` P ) /\ ( S ` .1. ) e. ( Base ` P ) ) )
62 61 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( P e. Grp /\ X e. ( Base ` P ) /\ ( S ` .1. ) e. ( Base ` P ) ) )
63 53 31 grpsubcl 
 |-  ( ( P e. Grp /\ X e. ( Base ` P ) /\ ( S ` .1. ) e. ( Base ` P ) ) -> ( X ( -g ` P ) ( S ` .1. ) ) e. ( Base ` P ) )
64 62 63 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( X ( -g ` P ) ( S ` .1. ) ) e. ( Base ` P ) )
65 5 53 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
66 64 65 eleqtrdi 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( X ( -g ` P ) ( S ` .1. ) ) e. ( Base ` G ) )
67 eqid 
 |-  ( Base ` G ) = ( Base ` G )
68 67 6 gsumconst 
 |-  ( ( G e. Mnd /\ N e. Fin /\ ( X ( -g ` P ) ( S ` .1. ) ) e. ( Base ` G ) ) -> ( G gsum ( k e. N |-> ( X ( -g ` P ) ( S ` .1. ) ) ) ) = ( ( # ` N ) .^ ( X ( -g ` P ) ( S ` .1. ) ) ) )
69 10 eqcomi 
 |-  ( -g ` P ) = .-
70 69 oveqi 
 |-  ( X ( -g ` P ) ( S ` .1. ) ) = ( X .- ( S ` .1. ) )
71 70 oveq2i 
 |-  ( ( # ` N ) .^ ( X ( -g ` P ) ( S ` .1. ) ) ) = ( ( # ` N ) .^ ( X .- ( S ` .1. ) ) )
72 68 71 eqtrdi 
 |-  ( ( G e. Mnd /\ N e. Fin /\ ( X ( -g ` P ) ( S ` .1. ) ) e. ( Base ` G ) ) -> ( G gsum ( k e. N |-> ( X ( -g ` P ) ( S ` .1. ) ) ) ) = ( ( # ` N ) .^ ( X .- ( S ` .1. ) ) ) )
73 49 11 66 72 syl3anc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( G gsum ( k e. N |-> ( X ( -g ` P ) ( S ` .1. ) ) ) ) = ( ( # ` N ) .^ ( X .- ( S ` .1. ) ) ) )
74 44 73 eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( G gsum ( k e. N |-> ( X ( -g ` P ) ( S ` ( k I k ) ) ) ) ) = ( ( # ` N ) .^ ( X .- ( S ` .1. ) ) ) )
75 33 74 eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( C ` I ) = ( ( # ` N ) .^ ( X .- ( S ` .1. ) ) ) )