# Metamath Proof Explorer

## Theorem pm2mpgrpiso

Description: The transformation of polynomial matrices into polynomials over matrices is an additive group isomorphism. (Contributed by AV, 17-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 pm2mpgrpiso ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{GrpIso}{Q}\right)$

### 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 9 10 pm2mpghm ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{GrpHom}{Q}\right)$
12 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
13 1 2 3 4 5 6 7 8 12 10 pm2mpf1o ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Q}}$
14 3 12 isgim ${⊢}{T}\in \left({C}\mathrm{GrpIso}{Q}\right)↔\left({T}\in \left({C}\mathrm{GrpHom}{Q}\right)\wedge {T}:{B}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Q}}\right)$
15 11 13 14 sylanbrc ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{GrpIso}{Q}\right)$