Metamath Proof Explorer

Theorem chp0mat

Description: The characteristic polynomial of the zero matrix. (Contributed by AV, 18-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 )
chp0mat.0 
|- .0. = ( 0g ` A )
Assertion chp0mat 
|- ( ( N e. Fin /\ R e. CRing ) -> ( C ` .0. ) = ( ( # ` N ) .^ 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 chp0mat.0 
 |-  .0. = ( 0g ` A )
8 simpl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> N e. Fin )
9 simpr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. CRing )
10 crngring 
 |-  ( R e. CRing -> R e. Ring )
11 3 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
12 10 11 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
13 ringgrp 
 |-  ( A e. Ring -> A e. Grp )
14 eqid 
 |-  ( Base ` A ) = ( Base ` A )
15 14 7 grpidcl 
 |-  ( A e. Grp -> .0. e. ( Base ` A ) )
16 12 13 15 3syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> .0. e. ( Base ` A ) )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 3 17 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( x e. N , y e. N |-> ( 0g ` R ) ) )
19 7 18 eqtrid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .0. = ( x e. N , y e. N |-> ( 0g ` R ) ) )
20 10 19 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> .0. = ( x e. N , y e. N |-> ( 0g ` R ) ) )
21 20 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) -> .0. = ( x e. N , y e. N |-> ( 0g ` R ) ) )
22 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) /\ ( x = i /\ y = j ) ) -> ( 0g ` R ) = ( 0g ` R ) )
23 simpl 
 |-  ( ( i e. N /\ j e. N ) -> i e. N )
24 23 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
25 simpr 
 |-  ( ( i e. N /\ j e. N ) -> j e. N )
26 25 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
27 fvexd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) -> ( 0g ` R ) e. _V )
28 21 22 24 26 27 ovmpod 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) -> ( i .0. j ) = ( 0g ` R ) )
29 28 a1d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( i e. N /\ j e. N ) ) -> ( i =/= j -> ( i .0. j ) = ( 0g ` R ) ) )
30 29 ralrimivva 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A. i e. N A. j e. N ( i =/= j -> ( i .0. j ) = ( 0g ` R ) ) )
31 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
32 eqid 
 |-  ( -g ` P ) = ( -g ` P )
33 1 2 3 31 14 4 17 5 32 chpdmat 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ .0. e. ( Base ` A ) ) /\ A. i e. N A. j e. N ( i =/= j -> ( i .0. j ) = ( 0g ` R ) ) ) -> ( C ` .0. ) = ( G gsum ( k e. N |-> ( X ( -g ` P ) ( ( algSc ` P ) ` ( k .0. k ) ) ) ) ) )
34 8 9 16 30 33 syl31anc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( C ` .0. ) = ( G gsum ( k e. N |-> ( X ( -g ` P ) ( ( algSc ` P ) ` ( k .0. k ) ) ) ) ) )
35 20 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> .0. = ( x e. N , y e. N |-> ( 0g ` R ) ) )
36 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) /\ ( x = k /\ y = k ) ) -> ( 0g ` R ) = ( 0g ` R ) )
37 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> k e. N )
38 fvexd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( 0g ` R ) e. _V )
39 35 36 37 37 38 ovmpod 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( k .0. k ) = ( 0g ` R ) )
40 39 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( ( algSc ` P ) ` ( k .0. k ) ) = ( ( algSc ` P ) ` ( 0g ` R ) ) )
41 10 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. Ring )
42 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
43 2 31 17 42 ply1scl0 
 |-  ( R e. Ring -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
44 41 43 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
45 44 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( ( algSc ` P ) ` ( 0g ` R ) ) = ( 0g ` P ) )
46 40 45 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( ( algSc ` P ) ` ( k .0. k ) ) = ( 0g ` P ) )
47 46 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( X ( -g ` P ) ( ( algSc ` P ) ` ( k .0. k ) ) ) = ( X ( -g ` P ) ( 0g ` P ) ) )
48 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
49 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
50 10 48 49 3syl 
 |-  ( R e. CRing -> P e. Grp )
51 50 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. Grp )
52 eqid 
 |-  ( Base ` P ) = ( Base ` P )
53 4 2 52 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
54 41 53 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` P ) )
55 51 54 jca 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( P e. Grp /\ X e. ( Base ` P ) ) )
56 55 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( P e. Grp /\ X e. ( Base ` P ) ) )
57 52 42 32 grpsubid1 
 |-  ( ( P e. Grp /\ X e. ( Base ` P ) ) -> ( X ( -g ` P ) ( 0g ` P ) ) = X )
58 56 57 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( X ( -g ` P ) ( 0g ` P ) ) = X )
59 47 58 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ k e. N ) -> ( X ( -g ` P ) ( ( algSc ` P ) ` ( k .0. k ) ) ) = X )
60 59 mpteq2dva 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( k e. N |-> ( X ( -g ` P ) ( ( algSc ` P ) ` ( k .0. k ) ) ) ) = ( k e. N |-> X ) )
61 60 oveq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( G gsum ( k e. N |-> ( X ( -g ` P ) ( ( algSc ` P ) ` ( k .0. k ) ) ) ) ) = ( G gsum ( k e. N |-> X ) ) )
62 2 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
63 5 crngmgp 
 |-  ( P e. CRing -> G e. CMnd )
64 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
65 62 63 64 3syl 
 |-  ( R e. CRing -> G e. Mnd )
66 65 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> G e. Mnd )
67 10 53 syl 
 |-  ( R e. CRing -> X e. ( Base ` P ) )
68 67 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` P ) )
69 5 52 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
70 68 69 eleqtrdi 
 |-  ( ( N e. Fin /\ R e. CRing ) -> X e. ( Base ` G ) )
71 eqid 
 |-  ( Base ` G ) = ( Base ` G )
72 71 6 gsumconst 
 |-  ( ( G e. Mnd /\ N e. Fin /\ X e. ( Base ` G ) ) -> ( G gsum ( k e. N |-> X ) ) = ( ( # ` N ) .^ X ) )
73 66 8 70 72 syl3anc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( G gsum ( k e. N |-> X ) ) = ( ( # ` N ) .^ X ) )
74 34 61 73 3eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( C ` .0. ) = ( ( # ` N ) .^ X ) )