Metamath Proof Explorer


Theorem chpmatval2

Description: The characteristic polynomial of a (square) matrix (expressed with the Leibnitz formula for the determinant). (Contributed by AV, 2-Aug-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 )
chpmatval2.y
|- Y = ( N Mat P )
chpmatval2.m1
|- .- = ( -g ` Y )
chpmatval2.x
|- X = ( var1 ` R )
chpmatval2.t1
|- .x. = ( .s ` Y )
chpmatval2.t
|- T = ( N matToPolyMat R )
chpmatval2.i
|- .1. = ( 1r ` Y )
chpmatval2.g
|- G = ( SymGrp ` N )
chpmatval2.h
|- H = ( Base ` G )
chpmatval2.z
|- Z = ( ZRHom ` P )
chpmatval2.s
|- S = ( pmSgn ` N )
chpmatval2.u
|- U = ( mulGrp ` P )
chpmatval2.rm
|- .X. = ( .r ` P )
Assertion chpmatval2
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( C ` M ) = ( P gsum ( p e. H |-> ( ( ( Z o. S ) ` p ) .X. ( U gsum ( x e. N |-> ( ( p ` x ) ( ( X .x. .1. ) .- ( T ` M ) ) x ) ) ) ) ) ) )

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 chpmatval2.y
 |-  Y = ( N Mat P )
6 chpmatval2.m1
 |-  .- = ( -g ` Y )
7 chpmatval2.x
 |-  X = ( var1 ` R )
8 chpmatval2.t1
 |-  .x. = ( .s ` Y )
9 chpmatval2.t
 |-  T = ( N matToPolyMat R )
10 chpmatval2.i
 |-  .1. = ( 1r ` Y )
11 chpmatval2.g
 |-  G = ( SymGrp ` N )
12 chpmatval2.h
 |-  H = ( Base ` G )
13 chpmatval2.z
 |-  Z = ( ZRHom ` P )
14 chpmatval2.s
 |-  S = ( pmSgn ` N )
15 chpmatval2.u
 |-  U = ( mulGrp ` P )
16 chpmatval2.rm
 |-  .X. = ( .r ` P )
17 eqid
 |-  ( N maDet P ) = ( N maDet P )
18 1 2 3 4 5 17 6 7 8 9 10 chpmatval
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( C ` M ) = ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) )
19 eqid
 |-  ( N Mat P ) = ( N Mat P )
20 5 fveq2i
 |-  ( -g ` Y ) = ( -g ` ( N Mat P ) )
21 6 20 eqtri
 |-  .- = ( -g ` ( N Mat P ) )
22 5 fveq2i
 |-  ( .s ` Y ) = ( .s ` ( N Mat P ) )
23 8 22 eqtri
 |-  .x. = ( .s ` ( N Mat P ) )
24 5 fveq2i
 |-  ( 1r ` Y ) = ( 1r ` ( N Mat P ) )
25 10 24 eqtri
 |-  .1. = ( 1r ` ( N Mat P ) )
26 eqid
 |-  ( ( X .x. .1. ) .- ( T ` M ) ) = ( ( X .x. .1. ) .- ( T ` M ) )
27 2 3 4 19 7 9 21 23 25 26 chmatcl
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` ( N Mat P ) ) )
28 5 eqcomi
 |-  ( N Mat P ) = Y
29 28 fveq2i
 |-  ( Base ` ( N Mat P ) ) = ( Base ` Y )
30 11 fveq2i
 |-  ( Base ` G ) = ( Base ` ( SymGrp ` N ) )
31 12 30 eqtri
 |-  H = ( Base ` ( SymGrp ` N ) )
32 17 5 29 31 13 14 16 15 mdetleib
 |-  ( ( ( X .x. .1. ) .- ( T ` M ) ) e. ( Base ` ( N Mat P ) ) -> ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) = ( P gsum ( p e. H |-> ( ( ( Z o. S ) ` p ) .X. ( U gsum ( x e. N |-> ( ( p ` x ) ( ( X .x. .1. ) .- ( T ` M ) ) x ) ) ) ) ) ) )
33 27 32 syl
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( ( N maDet P ) ` ( ( X .x. .1. ) .- ( T ` M ) ) ) = ( P gsum ( p e. H |-> ( ( ( Z o. S ) ` p ) .X. ( U gsum ( x e. N |-> ( ( p ` x ) ( ( X .x. .1. ) .- ( T ` M ) ) x ) ) ) ) ) ) )
34 18 33 eqtrd
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( C ` M ) = ( P gsum ( p e. H |-> ( ( ( Z o. S ) ` p ) .X. ( U gsum ( x e. N |-> ( ( p ` x ) ( ( X .x. .1. ) .- ( T ` M ) ) x ) ) ) ) ) ) )