# Metamath Proof Explorer

## Theorem pmmpric

Description: The ring of polynomial matrices over a ring is isomorphic to the ring of polynomials over matrices of the same dimension over the same ring. (Contributed by AV, 30-Dec-2019)

Ref Expression
Hypotheses pmmpric.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pmmpric.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pmmpric.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pmmpric.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
Assertion pmmpric ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}{\simeq }_{𝑟}{Q}$

### Proof

Step Hyp Ref Expression
1 pmmpric.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pmmpric.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pmmpric.a ${⊢}{A}={N}\mathrm{Mat}{R}$
4 pmmpric.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
5 eqid ${⊢}{N}\mathrm{pMatToMatPoly}{R}={N}\mathrm{pMatToMatPoly}{R}$
6 1 2 3 4 5 pm2mprngiso ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {N}\mathrm{pMatToMatPoly}{R}\in \left({C}\mathrm{RingIso}{Q}\right)$
7 6 ne0d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\mathrm{RingIso}{Q}\ne \varnothing$
8 brric ${⊢}{C}{\simeq }_{𝑟}{Q}↔{C}\mathrm{RingIso}{Q}\ne \varnothing$
9 7 8 sylibr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}{\simeq }_{𝑟}{Q}$