# Metamath Proof Explorer

## Theorem pm2mpf1o

Description: The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 14-Oct-2019)

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

### Proof

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