Metamath Proof Explorer

Theorem chpmatfval

Description: Value of the characteristic polynomial function. (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses chpmatfval.c 
|- C = ( N CharPlyMat R )
chpmatfval.a 
|- A = ( N Mat R )
chpmatfval.b 
|- B = ( Base ` A )
chpmatfval.p 
|- P = ( Poly1 ` R )
chpmatfval.y 
|- Y = ( N Mat P )
chpmatfval.d 
|- D = ( N maDet P )
chpmatfval.s 
|- .- = ( -g ` Y )
chpmatfval.x 
|- X = ( var1 ` R )
chpmatfval.m 
|- .x. = ( .s ` Y )
chpmatfval.t 
|- T = ( N matToPolyMat R )
chpmatfval.i 
|- .1. = ( 1r ` Y )
Assertion chpmatfval 
|- ( ( N e. Fin /\ R e. V ) -> C = ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chpmatfval.c 
 |-  C = ( N CharPlyMat R )
2 chpmatfval.a 
 |-  A = ( N Mat R )
3 chpmatfval.b 
 |-  B = ( Base ` A )
4 chpmatfval.p 
 |-  P = ( Poly1 ` R )
5 chpmatfval.y 
 |-  Y = ( N Mat P )
6 chpmatfval.d 
 |-  D = ( N maDet P )
7 chpmatfval.s 
 |-  .- = ( -g ` Y )
8 chpmatfval.x 
 |-  X = ( var1 ` R )
9 chpmatfval.m 
 |-  .x. = ( .s ` Y )
10 chpmatfval.t 
 |-  T = ( N matToPolyMat R )
11 chpmatfval.i 
 |-  .1. = ( 1r ` Y )
12 df-chpmat 
 |-  CharPlyMat = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) )
13 12 a1i 
 |-  ( ( N e. Fin /\ R e. V ) -> CharPlyMat = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) ) )
14 oveq12 
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = ( N Mat R ) )
15 14 2 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = A )
16 15 fveq2d 
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = ( Base ` A ) )
17 16 3 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = B )
18 simpl 
 |-  ( ( n = N /\ r = R ) -> n = N )
19 simpr 
 |-  ( ( n = N /\ r = R ) -> r = R )
20 19 fveq2d 
 |-  ( ( n = N /\ r = R ) -> ( Poly1 ` r ) = ( Poly1 ` R ) )
21 20 4 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( Poly1 ` r ) = P )
22 18 21 oveq12d 
 |-  ( ( n = N /\ r = R ) -> ( n maDet ( Poly1 ` r ) ) = ( N maDet P ) )
23 22 6 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( n maDet ( Poly1 ` r ) ) = D )
24 fveq2 
 |-  ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) )
25 24 adantl 
 |-  ( ( n = N /\ r = R ) -> ( Poly1 ` r ) = ( Poly1 ` R ) )
26 25 4 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( Poly1 ` r ) = P )
27 18 26 oveq12d 
 |-  ( ( n = N /\ r = R ) -> ( n Mat ( Poly1 ` r ) ) = ( N Mat P ) )
28 27 5 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( n Mat ( Poly1 ` r ) ) = Y )
29 28 fveq2d 
 |-  ( ( n = N /\ r = R ) -> ( -g ` ( n Mat ( Poly1 ` r ) ) ) = ( -g ` Y ) )
30 29 7 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( -g ` ( n Mat ( Poly1 ` r ) ) ) = .- )
31 28 fveq2d 
 |-  ( ( n = N /\ r = R ) -> ( .s ` ( n Mat ( Poly1 ` r ) ) ) = ( .s ` Y ) )
32 31 9 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( .s ` ( n Mat ( Poly1 ` r ) ) ) = .x. )
33 fveq2 
 |-  ( r = R -> ( var1 ` r ) = ( var1 ` R ) )
34 33 8 eqtr4di 
 |-  ( r = R -> ( var1 ` r ) = X )
35 34 adantl 
 |-  ( ( n = N /\ r = R ) -> ( var1 ` r ) = X )
36 28 fveq2d 
 |-  ( ( n = N /\ r = R ) -> ( 1r ` ( n Mat ( Poly1 ` r ) ) ) = ( 1r ` Y ) )
37 36 11 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( 1r ` ( n Mat ( Poly1 ` r ) ) ) = .1. )
38 32 35 37 oveq123d 
 |-  ( ( n = N /\ r = R ) -> ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) = ( X .x. .1. ) )
39 oveq12 
 |-  ( ( n = N /\ r = R ) -> ( n matToPolyMat r ) = ( N matToPolyMat R ) )
40 39 10 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( n matToPolyMat r ) = T )
41 40 fveq1d 
 |-  ( ( n = N /\ r = R ) -> ( ( n matToPolyMat r ) ` m ) = ( T ` m ) )
42 30 38 41 oveq123d 
 |-  ( ( n = N /\ r = R ) -> ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) = ( ( X .x. .1. ) .- ( T ` m ) ) )
43 23 42 fveq12d 
 |-  ( ( n = N /\ r = R ) -> ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) = ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) )
44 17 43 mpteq12dv 
 |-  ( ( n = N /\ r = R ) -> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) = ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) )
45 44 adantl 
 |-  ( ( ( N e. Fin /\ R e. V ) /\ ( n = N /\ r = R ) ) -> ( m e. ( Base ` ( n Mat r ) ) |-> ( ( n maDet ( Poly1 ` r ) ) ` ( ( ( var1 ` r ) ( .s ` ( n Mat ( Poly1 ` r ) ) ) ( 1r ` ( n Mat ( Poly1 ` r ) ) ) ) ( -g ` ( n Mat ( Poly1 ` r ) ) ) ( ( n matToPolyMat r ) ` m ) ) ) ) = ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) )
46 simpl 
 |-  ( ( N e. Fin /\ R e. V ) -> N e. Fin )
47 elex 
 |-  ( R e. V -> R e. _V )
48 47 adantl 
 |-  ( ( N e. Fin /\ R e. V ) -> R e. _V )
49 3 fvexi 
 |-  B e. _V
50 mptexg 
 |-  ( B e. _V -> ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) e. _V )
51 49 50 mp1i 
 |-  ( ( N e. Fin /\ R e. V ) -> ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) e. _V )
52 13 45 46 48 51 ovmpod 
 |-  ( ( N e. Fin /\ R e. V ) -> ( N CharPlyMat R ) = ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) )
53 1 52 eqtrid 
 |-  ( ( N e. Fin /\ R e. V ) -> C = ( m e. B |-> ( D ` ( ( X .x. .1. ) .- ( T ` m ) ) ) ) )