# Metamath Proof Explorer

## Theorem pm2mprhm

Description: The transformation of polynomial matrices into polynomials over matrices is a ring homomorphism. (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 pm2mprhm ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{RingHom}{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 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
7 3 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
8 4 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
9 7 8 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{Ring}$
10 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
11 eqid ${⊢}{\cdot }_{{Q}}={\cdot }_{{Q}}$
12 eqid ${⊢}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}={\cdot }_{{\mathrm{mulGrp}}_{{Q}}}$
13 eqid ${⊢}{\mathrm{var}}_{1}\left({A}\right)={\mathrm{var}}_{1}\left({A}\right)$
14 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
15 1 2 10 11 12 13 3 4 14 5 pm2mpghm ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{GrpHom}{Q}\right)$
16 1 2 3 4 5 pm2mpmhm ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({\mathrm{mulGrp}}_{{C}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{Q}}\right)$
17 15 16 jca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({T}\in \left({C}\mathrm{GrpHom}{Q}\right)\wedge {T}\in \left({\mathrm{mulGrp}}_{{C}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{Q}}\right)\right)$
18 eqid ${⊢}{\mathrm{mulGrp}}_{{C}}={\mathrm{mulGrp}}_{{C}}$
19 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
20 18 19 isrhm ${⊢}{T}\in \left({C}\mathrm{RingHom}{Q}\right)↔\left(\left({C}\in \mathrm{Ring}\wedge {Q}\in \mathrm{Ring}\right)\wedge \left({T}\in \left({C}\mathrm{GrpHom}{Q}\right)\wedge {T}\in \left({\mathrm{mulGrp}}_{{C}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{Q}}\right)\right)\right)$
21 6 9 17 20 syl21anbrc ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{RingHom}{Q}\right)$