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=CharPlyMatR
Assertion chpmat0d RRingC=1Poly1R

Proof

Step Hyp Ref Expression
1 chpmat0.c C=CharPlyMatR
2 0fin Fin
3 id RRingRRing
4 0ex V
5 4 snid
6 mat0dimbas0 RRingBaseMatR=
7 5 6 eleqtrrid RRingBaseMatR
8 eqid MatR=MatR
9 eqid BaseMatR=BaseMatR
10 eqid Poly1R=Poly1R
11 eqid MatPoly1R=MatPoly1R
12 eqid maDetPoly1R=maDetPoly1R
13 eqid -MatPoly1R=-MatPoly1R
14 eqid var1R=var1R
15 eqid MatPoly1R=MatPoly1R
16 eqid matToPolyMatR=matToPolyMatR
17 eqid 1MatPoly1R=1MatPoly1R
18 1 8 9 10 11 12 13 14 15 16 17 chpmatval FinRRingBaseMatRC=maDetPoly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR
19 2 3 7 18 mp3an2i RRingC=maDetPoly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR
20 10 ply1ring RRingPoly1RRing
21 mdet0pr Poly1RRingmaDetPoly1R=1Poly1R
22 21 fveq1d Poly1RRingmaDetPoly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR=1Poly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR
23 20 22 syl RRingmaDetPoly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR=1Poly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR
24 11 mat0dimid Poly1RRing1MatPoly1R=
25 20 24 syl RRing1MatPoly1R=
26 25 oveq2d RRingvar1RMatPoly1R1MatPoly1R=var1RMatPoly1R
27 eqid BasePoly1R=BasePoly1R
28 14 10 27 vr1cl RRingvar1RBasePoly1R
29 11 mat0dimscm Poly1RRingvar1RBasePoly1Rvar1RMatPoly1R=
30 20 28 29 syl2anc RRingvar1RMatPoly1R=
31 26 30 eqtrd RRingvar1RMatPoly1R1MatPoly1R=
32 d0mat2pmat RRingmatToPolyMatR=
33 31 32 oveq12d RRingvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR=-MatPoly1R
34 11 matring FinPoly1RRingMatPoly1RRing
35 2 20 34 sylancr RRingMatPoly1RRing
36 ringgrp MatPoly1RRingMatPoly1RGrp
37 35 36 syl RRingMatPoly1RGrp
38 mat0dimbas0 Poly1RRingBaseMatPoly1R=
39 20 38 syl RRingBaseMatPoly1R=
40 5 39 eleqtrrid RRingBaseMatPoly1R
41 eqid BaseMatPoly1R=BaseMatPoly1R
42 eqid 0MatPoly1R=0MatPoly1R
43 41 42 13 grpsubid MatPoly1RGrpBaseMatPoly1R-MatPoly1R=0MatPoly1R
44 37 40 43 syl2anc RRing-MatPoly1R=0MatPoly1R
45 33 44 eqtrd RRingvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR=0MatPoly1R
46 45 fveq2d RRing1Poly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR=1Poly1R0MatPoly1R
47 11 mat0dim0 Poly1RRing0MatPoly1R=
48 20 47 syl RRing0MatPoly1R=
49 48 fveq2d RRing1Poly1R0MatPoly1R=1Poly1R
50 fvex 1Poly1RV
51 4 50 fvsn 1Poly1R=1Poly1R
52 49 51 eqtrdi RRing1Poly1R0MatPoly1R=1Poly1R
53 46 52 eqtrd RRing1Poly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR=1Poly1R
54 23 53 eqtrd RRingmaDetPoly1Rvar1RMatPoly1R1MatPoly1R-MatPoly1RmatToPolyMatR=1Poly1R
55 19 54 eqtrd RRingC=1Poly1R