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 = Poly 1 R
chpmatfval.y Y = N Mat P
chpmatfval.d D = N maDet P
chpmatfval.s - ˙ = - Y
chpmatfval.x X = var 1 R
chpmatfval.m · ˙ = Y
chpmatfval.t T = N matToPolyMat R
chpmatfval.i 1 ˙ = 1 Y
Assertion chpmatfval N Fin R V C = m B D 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 = Poly 1 R
5 chpmatfval.y Y = N Mat P
6 chpmatfval.d D = N maDet P
7 chpmatfval.s - ˙ = - Y
8 chpmatfval.x X = var 1 R
9 chpmatfval.m · ˙ = Y
10 chpmatfval.t T = N matToPolyMat R
11 chpmatfval.i 1 ˙ = 1 Y
12 df-chpmat CharPlyMat = n Fin , r V m Base n Mat r n maDet Poly 1 r var 1 r n Mat Poly 1 r 1 n Mat Poly 1 r - n Mat Poly 1 r n matToPolyMat r m
13 12 a1i N Fin R V CharPlyMat = n Fin , r V m Base n Mat r n maDet Poly 1 r var 1 r n Mat Poly 1 r 1 n Mat Poly 1 r - n Mat Poly 1 r n matToPolyMat r m
14 oveq12 n = N r = R n Mat r = N Mat R
15 14 2 syl6eqr n = N r = R n Mat r = A
16 15 fveq2d n = N r = R Base n Mat r = Base A
17 16 3 syl6eqr 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 Poly 1 r = Poly 1 R
21 20 4 syl6eqr n = N r = R Poly 1 r = P
22 18 21 oveq12d n = N r = R n maDet Poly 1 r = N maDet P
23 22 6 syl6eqr n = N r = R n maDet Poly 1 r = D
24 fveq2 r = R Poly 1 r = Poly 1 R
25 24 adantl n = N r = R Poly 1 r = Poly 1 R
26 25 4 syl6eqr n = N r = R Poly 1 r = P
27 18 26 oveq12d n = N r = R n Mat Poly 1 r = N Mat P
28 27 5 syl6eqr n = N r = R n Mat Poly 1 r = Y
29 28 fveq2d n = N r = R - n Mat Poly 1 r = - Y
30 29 7 syl6eqr n = N r = R - n Mat Poly 1 r = - ˙
31 28 fveq2d n = N r = R n Mat Poly 1 r = Y
32 31 9 syl6eqr n = N r = R n Mat Poly 1 r = · ˙
33 fveq2 r = R var 1 r = var 1 R
34 33 8 syl6eqr r = R var 1 r = X
35 34 adantl n = N r = R var 1 r = X
36 28 fveq2d n = N r = R 1 n Mat Poly 1 r = 1 Y
37 36 11 syl6eqr n = N r = R 1 n Mat Poly 1 r = 1 ˙
38 32 35 37 oveq123d n = N r = R var 1 r n Mat Poly 1 r 1 n Mat Poly 1 r = X · ˙ 1 ˙
39 oveq12 n = N r = R n matToPolyMat r = N matToPolyMat R
40 39 10 syl6eqr 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 var 1 r n Mat Poly 1 r 1 n Mat Poly 1 r - n Mat Poly 1 r n matToPolyMat r m = X · ˙ 1 ˙ - ˙ T m
43 23 42 fveq12d n = N r = R n maDet Poly 1 r var 1 r n Mat Poly 1 r 1 n Mat Poly 1 r - n Mat Poly 1 r n matToPolyMat r m = D X · ˙ 1 ˙ - ˙ T m
44 17 43 mpteq12dv n = N r = R m Base n Mat r n maDet Poly 1 r var 1 r n Mat Poly 1 r 1 n Mat Poly 1 r - n Mat Poly 1 r n matToPolyMat r m = m B D X · ˙ 1 ˙ - ˙ T m
45 44 adantl N Fin R V n = N r = R m Base n Mat r n maDet Poly 1 r var 1 r n Mat Poly 1 r 1 n Mat Poly 1 r - n Mat Poly 1 r n matToPolyMat r m = m B D X · ˙ 1 ˙ - ˙ T m
46 simpl N Fin R V N Fin
47 elex R V R V
48 47 adantl N Fin R V R V
49 3 fvexi B V
50 mptexg B V m B D X · ˙ 1 ˙ - ˙ T m V
51 49 50 mp1i N Fin R V m B D X · ˙ 1 ˙ - ˙ T m V
52 13 45 46 48 51 ovmpod N Fin R V N CharPlyMat R = m B D X · ˙ 1 ˙ - ˙ T m
53 1 52 syl5eq N Fin R V C = m B D X · ˙ 1 ˙ - ˙ T m