Metamath Proof Explorer

Theorem chpmat0d

Description: The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019)

Ref Expression
Hypothesis chpmat0.c 
|- C = ( (/) CharPlyMat R )
Assertion chpmat0d 
|- ( R e. Ring -> ( C ` (/) ) = ( 1r ` ( Poly1 ` R ) ) )

Proof

Step Hyp Ref Expression
1 chpmat0.c 
 |-  C = ( (/) CharPlyMat R )
2 0fin 
 |-  (/) e. Fin
3 id 
 |-  ( R e. Ring -> R e. Ring )
4 0ex 
 |-  (/) e. _V
5 4 snid 
 |-  (/) e. { (/) }
6 mat0dimbas0 
 |-  ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } )
7 5 6 eleqtrrid 
 |-  ( R e. Ring -> (/) e. ( Base ` ( (/) Mat R ) ) )
8 eqid 
 |-  ( (/) Mat R ) = ( (/) Mat R )
9 eqid 
 |-  ( Base ` ( (/) Mat R ) ) = ( Base ` ( (/) Mat R ) )
10 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
11 eqid 
 |-  ( (/) Mat ( Poly1 ` R ) ) = ( (/) Mat ( Poly1 ` R ) )
12 eqid 
 |-  ( (/) maDet ( Poly1 ` R ) ) = ( (/) maDet ( Poly1 ` R ) )
13 eqid 
 |-  ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) = ( -g ` ( (/) Mat ( Poly1 ` R ) ) )
14 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
15 eqid 
 |-  ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) = ( .s ` ( (/) Mat ( Poly1 ` R ) ) )
16 eqid 
 |-  ( (/) matToPolyMat R ) = ( (/) matToPolyMat R )
17 eqid 
 |-  ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) = ( 1r ` ( (/) Mat ( Poly1 ` R ) ) )
18 1 8 9 10 11 12 13 14 15 16 17 chpmatval 
 |-  ( ( (/) e. Fin /\ R e. Ring /\ (/) e. ( Base ` ( (/) Mat R ) ) ) -> ( C ` (/) ) = ( ( (/) maDet ( Poly1 ` R ) ) ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) )
19 2 3 7 18 mp3an2i 
 |-  ( R e. Ring -> ( C ` (/) ) = ( ( (/) maDet ( Poly1 ` R ) ) ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) )
20 10 ply1ring 
 |-  ( R e. Ring -> ( Poly1 ` R ) e. Ring )
21 mdet0pr 
 |-  ( ( Poly1 ` R ) e. Ring -> ( (/) maDet ( Poly1 ` R ) ) = { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } )
22 21 fveq1d 
 |-  ( ( Poly1 ` R ) e. Ring -> ( ( (/) maDet ( Poly1 ` R ) ) ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) = ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) )
23 20 22 syl 
 |-  ( R e. Ring -> ( ( (/) maDet ( Poly1 ` R ) ) ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) = ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) )
24 11 mat0dimid 
 |-  ( ( Poly1 ` R ) e. Ring -> ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) = (/) )
25 20 24 syl 
 |-  ( R e. Ring -> ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) = (/) )
26 25 oveq2d 
 |-  ( R e. Ring -> ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) = ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) (/) ) )
27 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
28 14 10 27 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) )
29 11 mat0dimscm 
 |-  ( ( ( Poly1 ` R ) e. Ring /\ ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) (/) ) = (/) )
30 20 28 29 syl2anc 
 |-  ( R e. Ring -> ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) (/) ) = (/) )
31 26 30 eqtrd 
 |-  ( R e. Ring -> ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) = (/) )
32 d0mat2pmat 
 |-  ( R e. Ring -> ( ( (/) matToPolyMat R ) ` (/) ) = (/) )
33 31 32 oveq12d 
 |-  ( R e. Ring -> ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) = ( (/) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) (/) ) )
34 11 matring 
 |-  ( ( (/) e. Fin /\ ( Poly1 ` R ) e. Ring ) -> ( (/) Mat ( Poly1 ` R ) ) e. Ring )
35 2 20 34 sylancr 
 |-  ( R e. Ring -> ( (/) Mat ( Poly1 ` R ) ) e. Ring )
36 ringgrp 
 |-  ( ( (/) Mat ( Poly1 ` R ) ) e. Ring -> ( (/) Mat ( Poly1 ` R ) ) e. Grp )
37 35 36 syl 
 |-  ( R e. Ring -> ( (/) Mat ( Poly1 ` R ) ) e. Grp )
38 mat0dimbas0 
 |-  ( ( Poly1 ` R ) e. Ring -> ( Base ` ( (/) Mat ( Poly1 ` R ) ) ) = { (/) } )
39 20 38 syl 
 |-  ( R e. Ring -> ( Base ` ( (/) Mat ( Poly1 ` R ) ) ) = { (/) } )
40 5 39 eleqtrrid 
 |-  ( R e. Ring -> (/) e. ( Base ` ( (/) Mat ( Poly1 ` R ) ) ) )
41 eqid 
 |-  ( Base ` ( (/) Mat ( Poly1 ` R ) ) ) = ( Base ` ( (/) Mat ( Poly1 ` R ) ) )
42 eqid 
 |-  ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) = ( 0g ` ( (/) Mat ( Poly1 ` R ) ) )
43 41 42 13 grpsubid 
 |-  ( ( ( (/) Mat ( Poly1 ` R ) ) e. Grp /\ (/) e. ( Base ` ( (/) Mat ( Poly1 ` R ) ) ) ) -> ( (/) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) (/) ) = ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) )
44 37 40 43 syl2anc 
 |-  ( R e. Ring -> ( (/) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) (/) ) = ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) )
45 33 44 eqtrd 
 |-  ( R e. Ring -> ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) = ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) )
46 45 fveq2d 
 |-  ( R e. Ring -> ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) = ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) ) )
47 11 mat0dim0 
 |-  ( ( Poly1 ` R ) e. Ring -> ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) = (/) )
48 20 47 syl 
 |-  ( R e. Ring -> ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) = (/) )
49 48 fveq2d 
 |-  ( R e. Ring -> ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) ) = ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` (/) ) )
50 fvex 
 |-  ( 1r ` ( Poly1 ` R ) ) e. _V
51 4 50 fvsn 
 |-  ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` (/) ) = ( 1r ` ( Poly1 ` R ) )
52 49 51 eqtrdi 
 |-  ( R e. Ring -> ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` ( 0g ` ( (/) Mat ( Poly1 ` R ) ) ) ) = ( 1r ` ( Poly1 ` R ) ) )
53 46 52 eqtrd 
 |-  ( R e. Ring -> ( { <. (/) , ( 1r ` ( Poly1 ` R ) ) >. } ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) = ( 1r ` ( Poly1 ` R ) ) )
54 23 53 eqtrd 
 |-  ( R e. Ring -> ( ( (/) maDet ( Poly1 ` R ) ) ` ( ( ( var1 ` R ) ( .s ` ( (/) Mat ( Poly1 ` R ) ) ) ( 1r ` ( (/) Mat ( Poly1 ` R ) ) ) ) ( -g ` ( (/) Mat ( Poly1 ` R ) ) ) ( ( (/) matToPolyMat R ) ` (/) ) ) ) = ( 1r ` ( Poly1 ` R ) ) )
55 19 54 eqtrd 
 |-  ( R e. Ring -> ( C ` (/) ) = ( 1r ` ( Poly1 ` R ) ) )