Metamath Proof Explorer

Theorem chpmat1d

Description: The characteristic polynomial of a matrix with dimension 1. (Contributed by AV, 7-Aug-2019)

Ref Expression
Hypotheses chpmat1d.c 
|- C = ( N CharPlyMat R )
chpmat1d.p 
|- P = ( Poly1 ` R )
chpmat1d.a 
|- A = ( N Mat R )
chpmat1d.b 
|- B = ( Base ` A )
chpmat1d.x 
|- X = ( var1 ` R )
chpmat1d.z 
|- .- = ( -g ` P )
chpmat1d.s 
|- S = ( algSc ` P )
Assertion chpmat1d 
|- ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( C ` M ) = ( X .- ( S ` ( I M I ) ) ) )

Proof

Step Hyp Ref Expression
1 chpmat1d.c 
 |-  C = ( N CharPlyMat R )
2 chpmat1d.p 
 |-  P = ( Poly1 ` R )
3 chpmat1d.a 
 |-  A = ( N Mat R )
4 chpmat1d.b 
 |-  B = ( Base ` A )
5 chpmat1d.x 
 |-  X = ( var1 ` R )
6 chpmat1d.z 
 |-  .- = ( -g ` P )
7 chpmat1d.s 
 |-  S = ( algSc ` P )
8 snfi 
 |-  { I } e. Fin
9 eleq1 
 |-  ( N = { I } -> ( N e. Fin <-> { I } e. Fin ) )
10 8 9 mpbiri 
 |-  ( N = { I } -> N e. Fin )
11 10 adantr 
 |-  ( ( N = { I } /\ I e. V ) -> N e. Fin )
12 11 3ad2ant2 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> N e. Fin )
13 simp1 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> R e. CRing )
14 simp3 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> M e. B )
15 eqid 
 |-  ( N Mat P ) = ( N Mat P )
16 eqid 
 |-  ( N maDet P ) = ( N maDet P )
17 eqid 
 |-  ( -g ` ( N Mat P ) ) = ( -g ` ( N Mat P ) )
18 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
19 eqid 
 |-  ( .s ` ( N Mat P ) ) = ( .s ` ( N Mat P ) )
20 eqid 
 |-  ( N matToPolyMat R ) = ( N matToPolyMat R )
21 eqid 
 |-  ( 1r ` ( N Mat P ) ) = ( 1r ` ( N Mat P ) )
22 1 3 4 2 15 16 17 18 19 20 21 chpmatval 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) = ( ( N maDet P ) ` ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) )
23 12 13 14 22 syl3anc 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( C ` M ) = ( ( N maDet P ) ` ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) )
24 2 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
25 24 3ad2ant1 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> P e. CRing )
26 simp2 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( N = { I } /\ I e. V ) )
27 crngring 
 |-  ( R e. CRing -> R e. Ring )
28 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
29 27 28 syl 
 |-  ( R e. CRing -> P e. Ring )
30 29 3ad2ant1 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> P e. Ring )
31 15 matring 
 |-  ( ( N e. Fin /\ P e. Ring ) -> ( N Mat P ) e. Ring )
32 12 30 31 syl2anc 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( N Mat P ) e. Ring )
33 ringgrp 
 |-  ( ( N Mat P ) e. Ring -> ( N Mat P ) e. Grp )
34 32 33 syl 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( N Mat P ) e. Grp )
35 15 matlmod 
 |-  ( ( N e. Fin /\ P e. Ring ) -> ( N Mat P ) e. LMod )
36 12 30 35 syl2anc 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( N Mat P ) e. LMod )
37 27 3ad2ant1 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> R e. Ring )
38 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
39 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
40 18 38 39 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) )
41 37 40 syl 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) )
42 38 ply1crng 
 |-  ( R e. CRing -> ( Poly1 ` R ) e. CRing )
43 42 3ad2ant1 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( Poly1 ` R ) e. CRing )
44 2 oveq2i 
 |-  ( N Mat P ) = ( N Mat ( Poly1 ` R ) )
45 44 matsca2 
 |-  ( ( N e. Fin /\ ( Poly1 ` R ) e. CRing ) -> ( Poly1 ` R ) = ( Scalar ` ( N Mat P ) ) )
46 12 43 45 syl2anc 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( Poly1 ` R ) = ( Scalar ` ( N Mat P ) ) )
47 46 eqcomd 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( Scalar ` ( N Mat P ) ) = ( Poly1 ` R ) )
48 47 fveq2d 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( Base ` ( Scalar ` ( N Mat P ) ) ) = ( Base ` ( Poly1 ` R ) ) )
49 41 48 eleqtrrd 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( var1 ` R ) e. ( Base ` ( Scalar ` ( N Mat P ) ) ) )
50 eqid 
 |-  ( Base ` ( N Mat P ) ) = ( Base ` ( N Mat P ) )
51 50 21 ringidcl 
 |-  ( ( N Mat P ) e. Ring -> ( 1r ` ( N Mat P ) ) e. ( Base ` ( N Mat P ) ) )
52 32 51 syl 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( 1r ` ( N Mat P ) ) e. ( Base ` ( N Mat P ) ) )
53 eqid 
 |-  ( Scalar ` ( N Mat P ) ) = ( Scalar ` ( N Mat P ) )
54 eqid 
 |-  ( Base ` ( Scalar ` ( N Mat P ) ) ) = ( Base ` ( Scalar ` ( N Mat P ) ) )
55 50 53 19 54 lmodvscl 
 |-  ( ( ( N Mat P ) e. LMod /\ ( var1 ` R ) e. ( Base ` ( Scalar ` ( N Mat P ) ) ) /\ ( 1r ` ( N Mat P ) ) e. ( Base ` ( N Mat P ) ) ) -> ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) e. ( Base ` ( N Mat P ) ) )
56 36 49 52 55 syl3anc 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) e. ( Base ` ( N Mat P ) ) )
57 20 3 4 2 15 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( N matToPolyMat R ) ` M ) e. ( Base ` ( N Mat P ) ) )
58 12 37 14 57 syl3anc 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( N matToPolyMat R ) ` M ) e. ( Base ` ( N Mat P ) ) )
59 50 17 grpsubcl 
 |-  ( ( ( N Mat P ) e. Grp /\ ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) e. ( Base ` ( N Mat P ) ) /\ ( ( N matToPolyMat R ) ` M ) e. ( Base ` ( N Mat P ) ) ) -> ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) e. ( Base ` ( N Mat P ) ) )
60 34 56 58 59 syl3anc 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) e. ( Base ` ( N Mat P ) ) )
61 16 15 50 m1detdiag 
 |-  ( ( P e. CRing /\ ( N = { I } /\ I e. V ) /\ ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) e. ( Base ` ( N Mat P ) ) ) -> ( ( N maDet P ) ` ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) = ( I ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) I ) )
62 25 26 60 61 syl3anc 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( N maDet P ) ` ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) = ( I ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) I ) )
63 5 eqcomi 
 |-  ( var1 ` R ) = X
64 63 a1i 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( var1 ` R ) = X )
65 64 oveq1d 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) = ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) )
66 65 oveq1d 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) = ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) )
67 66 oveqd 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) I ) = ( I ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) I ) )
68 1 2 3 4 5 6 7 15 20 chpmat1dlem 
 |-  ( ( R e. Ring /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) I ) = ( X .- ( S ` ( I M I ) ) ) )
69 27 68 syl3an1 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I ( ( X ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) I ) = ( X .- ( S ` ( I M I ) ) ) )
70 67 69 eqtrd 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( I ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) I ) = ( X .- ( S ` ( I M I ) ) ) )
71 62 70 eqtrd 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( ( N maDet P ) ` ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) = ( X .- ( S ` ( I M I ) ) ) )
72 23 71 eqtrd 
 |-  ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( C ` M ) = ( X .- ( S ` ( I M I ) ) ) )