# 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}\mathrm{CharPlyMat}{R}$
chpmatfval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
chpmatfval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
chpmatfval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
chpmatfval.y ${⊢}{Y}={N}\mathrm{Mat}{P}$
chpmatfval.d ${⊢}{D}={N}\mathrm{maDet}{P}$
chpmatfval.s
chpmatfval.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
chpmatfval.m
chpmatfval.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
chpmatfval.i
Assertion chpmatfval

### Proof

Step Hyp Ref Expression
1 chpmatfval.c ${⊢}{C}={N}\mathrm{CharPlyMat}{R}$
2 chpmatfval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
3 chpmatfval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 chpmatfval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
5 chpmatfval.y ${⊢}{Y}={N}\mathrm{Mat}{P}$
6 chpmatfval.d ${⊢}{D}={N}\mathrm{maDet}{P}$
7 chpmatfval.s
8 chpmatfval.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
9 chpmatfval.m
10 chpmatfval.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
11 chpmatfval.i
12 df-chpmat ${⊢}\mathrm{CharPlyMat}=\left({n}\in \mathrm{Fin},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({n}\mathrm{maDet}{\mathrm{Poly}}_{1}\left({r}\right)\right)\left(\left({\mathrm{var}}_{1}\left({r}\right){\cdot }_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}{1}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}\right){-}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}\left({n}\mathrm{matToPolyMat}{r}\right)\left({m}\right)\right)\right)\right)$
13 12 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to \mathrm{CharPlyMat}=\left({n}\in \mathrm{Fin},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({n}\mathrm{maDet}{\mathrm{Poly}}_{1}\left({r}\right)\right)\left(\left({\mathrm{var}}_{1}\left({r}\right){\cdot }_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}{1}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}\right){-}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}\left({n}\mathrm{matToPolyMat}{r}\right)\left({m}\right)\right)\right)\right)$
14 oveq12 ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{Mat}{r}={N}\mathrm{Mat}{R}$
15 14 2 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{Mat}{r}={A}$
16 15 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}={\mathrm{Base}}_{{A}}$
17 16 3 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}={B}$
18 simpl ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}={N}$
19 simpr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {r}={R}$
20 19 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Poly}}_{1}\left({r}\right)={\mathrm{Poly}}_{1}\left({R}\right)$
21 20 4 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Poly}}_{1}\left({r}\right)={P}$
22 18 21 oveq12d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{maDet}{\mathrm{Poly}}_{1}\left({r}\right)={N}\mathrm{maDet}{P}$
23 22 6 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{maDet}{\mathrm{Poly}}_{1}\left({r}\right)={D}$
24 fveq2 ${⊢}{r}={R}\to {\mathrm{Poly}}_{1}\left({r}\right)={\mathrm{Poly}}_{1}\left({R}\right)$
25 24 adantl ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Poly}}_{1}\left({r}\right)={\mathrm{Poly}}_{1}\left({R}\right)$
26 25 4 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Poly}}_{1}\left({r}\right)={P}$
27 18 26 oveq12d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)={N}\mathrm{Mat}{P}$
28 27 5 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)={Y}$
29 28 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {-}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}={-}_{{Y}}$
30 29 7 syl6eqr
31 28 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\cdot }_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}={\cdot }_{{Y}}$
32 31 9 syl6eqr
33 fveq2 ${⊢}{r}={R}\to {\mathrm{var}}_{1}\left({r}\right)={\mathrm{var}}_{1}\left({R}\right)$
34 33 8 syl6eqr ${⊢}{r}={R}\to {\mathrm{var}}_{1}\left({r}\right)={X}$
35 34 adantl ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{var}}_{1}\left({r}\right)={X}$
36 28 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {1}_{\left({n}\mathrm{Mat}{\mathrm{Poly}}_{1}\left({r}\right)\right)}={1}_{{Y}}$
37 36 11 syl6eqr
38 32 35 37 oveq123d
39 oveq12 ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{matToPolyMat}{r}={N}\mathrm{matToPolyMat}{R}$
40 39 10 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{matToPolyMat}{r}={T}$
41 40 fveq1d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to \left({n}\mathrm{matToPolyMat}{r}\right)\left({m}\right)={T}\left({m}\right)$
42 30 38 41 oveq123d
43 23 42 fveq12d
44 17 43 mpteq12dv
46 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {N}\in \mathrm{Fin}$
47 elex ${⊢}{R}\in {V}\to {R}\in \mathrm{V}$
48 47 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {R}\in \mathrm{V}$
49 3 fvexi ${⊢}{B}\in \mathrm{V}$