Metamath Proof Explorer

Theorem chpmatply1

Description: The characteristic polynomial of a (square) matrix over a commutative ring is a polynomial, see also the following remark in Lang, p. 561: "[the characteristic polynomial] is an element of k[t". (Contributed by AV, 2-Aug-2019) (Proof shortened by AV, 29-Nov-2019)

Ref Expression
Hypotheses chpmatply1.c 
|- C = ( N CharPlyMat R )
chpmatply1.a 
|- A = ( N Mat R )
chpmatply1.b 
|- B = ( Base ` A )
chpmatply1.p 
|- P = ( Poly1 ` R )
chpmatply1.e 
|- E = ( Base ` P )
Assertion chpmatply1 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) e. E )

Proof

Step Hyp Ref Expression
1 chpmatply1.c 
 |-  C = ( N CharPlyMat R )
2 chpmatply1.a 
 |-  A = ( N Mat R )
3 chpmatply1.b 
 |-  B = ( Base ` A )
4 chpmatply1.p 
 |-  P = ( Poly1 ` R )
5 chpmatply1.e 
 |-  E = ( Base ` P )
6 eqid 
 |-  ( N Mat P ) = ( N Mat P )
7 eqid 
 |-  ( N maDet P ) = ( N maDet P )
8 eqid 
 |-  ( -g ` ( N Mat P ) ) = ( -g ` ( N Mat P ) )
9 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
10 eqid 
 |-  ( .s ` ( N Mat P ) ) = ( .s ` ( N Mat P ) )
11 eqid 
 |-  ( N matToPolyMat R ) = ( N matToPolyMat R )
12 eqid 
 |-  ( 1r ` ( N Mat P ) ) = ( 1r ` ( N Mat P ) )
13 1 2 3 4 6 7 8 9 10 11 12 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 ) ) ) )
14 4 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
15 14 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. CRing )
16 crngring 
 |-  ( R e. CRing -> R e. Ring )
17 eqid 
 |-  ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) = ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) )
18 2 3 4 6 9 11 8 10 12 17 chmatcl 
 |-  ( ( N e. Fin /\ R e. Ring /\ 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 ) ) )
19 16 18 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ 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 ) ) )
20 eqid 
 |-  ( Base ` ( N Mat P ) ) = ( Base ` ( N Mat P ) )
21 7 6 20 5 mdetcl 
 |-  ( ( P e. CRing /\ ( ( ( 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 ) ) ) e. E )
22 15 19 21 syl2anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( N maDet P ) ` ( ( ( var1 ` R ) ( .s ` ( N Mat P ) ) ( 1r ` ( N Mat P ) ) ) ( -g ` ( N Mat P ) ) ( ( N matToPolyMat R ) ` M ) ) ) e. E )
23 13 22 eqeltrd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) e. E )