# Metamath Proof Explorer

## Theorem pm2mprngiso

Description: The transformation of polynomial matrices into polynomials over matrices is a ring isomorphism. (Contributed by AV, 22-Oct-2019)

Ref Expression
Hypotheses pm2mpmhm.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpmhm.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpmhm.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpmhm.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
pm2mpmhm.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
Assertion pm2mprngiso ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{RingIso}{Q}\right)$

### Proof

Step Hyp Ref Expression
1 pm2mpmhm.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpmhm.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpmhm.a ${⊢}{A}={N}\mathrm{Mat}{R}$
4 pm2mpmhm.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
5 pm2mpmhm.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
6 1 2 3 4 5 pm2mprhm ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{RingHom}{Q}\right)$
7 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
8 eqid ${⊢}{\cdot }_{{Q}}={\cdot }_{{Q}}$
9 eqid ${⊢}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}={\cdot }_{{\mathrm{mulGrp}}_{{Q}}}$
10 eqid ${⊢}{\mathrm{var}}_{1}\left({A}\right)={\mathrm{var}}_{1}\left({A}\right)$
11 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
12 1 2 7 8 9 10 3 4 11 5 pm2mpf1o ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{\mathrm{Base}}_{{C}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Q}}$
13 1 2 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
14 3 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
15 4 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
16 14 15 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{Ring}$
17 7 11 isrim ${⊢}\left({C}\in \mathrm{Ring}\wedge {Q}\in \mathrm{Ring}\right)\to \left({T}\in \left({C}\mathrm{RingIso}{Q}\right)↔\left({T}\in \left({C}\mathrm{RingHom}{Q}\right)\wedge {T}:{\mathrm{Base}}_{{C}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Q}}\right)\right)$
18 13 16 17 syl2anc ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({T}\in \left({C}\mathrm{RingIso}{Q}\right)↔\left({T}\in \left({C}\mathrm{RingHom}{Q}\right)\wedge {T}:{\mathrm{Base}}_{{C}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Q}}\right)\right)$
19 6 12 18 mpbir2and ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{RingIso}{Q}\right)$