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 ) ) ) ) ) ) )