# Metamath Proof Explorer

## Theorem pm2mpf

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019) (Revised by AV, 5-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpval.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pm2mpval.m
pm2mpval.e
pm2mpval.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
pm2mpval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpval.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
pm2mpval.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
pm2mpcl.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
Assertion pm2mpf ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}⟶{L}$

### Proof

Step Hyp Ref Expression
1 pm2mpval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpval.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pm2mpval.m
5 pm2mpval.e
6 pm2mpval.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
7 pm2mpval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
8 pm2mpval.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
9 pm2mpval.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
10 pm2mpcl.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
11 ovexd
12 1 2 3 4 5 6 7 8 9 pm2mpval
13 1 2 3 4 5 6 7 8 9 10 pm2mpcl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {b}\in {B}\right)\to {T}\left({b}\right)\in {L}$
14 13 3expa ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {b}\in {B}\right)\to {T}\left({b}\right)\in {L}$
15 11 12 14 fmpt2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}⟶{L}$