# Metamath Proof Explorer

## Theorem pm2mpmhm

Description: The transformation of polynomial matrices into polynomials over matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 22-Oct-2019) (Revised by AV, 6-Dec-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 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)$

### 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 eqid ${⊢}{\mathrm{mulGrp}}_{{C}}={\mathrm{mulGrp}}_{{C}}$
8 7 ringmgp ${⊢}{C}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{C}}\in \mathrm{Mnd}$
9 6 8 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\mathrm{mulGrp}}_{{C}}\in \mathrm{Mnd}$
10 3 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
11 4 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
12 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
13 12 ringmgp ${⊢}{Q}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}$
14 10 11 13 3syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}$
15 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
16 7 15 mgpbas ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}$
17 16 eqcomi ${⊢}{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}={\mathrm{Base}}_{{C}}$
18 eqid ${⊢}{\cdot }_{{Q}}={\cdot }_{{Q}}$
19 eqid ${⊢}{\cdot }_{{\mathrm{mulGrp}}_{{Q}}}={\cdot }_{{\mathrm{mulGrp}}_{{Q}}}$
20 eqid ${⊢}{\mathrm{var}}_{1}\left({A}\right)={\mathrm{var}}_{1}\left({A}\right)$
21 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
22 12 21 mgpbas ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}$
23 22 eqcomi ${⊢}{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}={\mathrm{Base}}_{{Q}}$
24 1 2 17 18 19 20 3 4 5 23 pm2mpf ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}⟶{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}$
25 1 2 3 4 5 17 pm2mpmhmlem2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \forall {x}\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}\phantom{\rule{.4em}{0ex}}{T}\left({x}{\cdot }_{{C}}{y}\right)={T}\left({x}\right){\cdot }_{{Q}}{T}\left({y}\right)$
26 1 2 15 18 19 20 3 4 5 idpm2idmp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\left({1}_{{C}}\right)={1}_{{Q}}$
27 24 25 26 3jca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({T}:{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}⟶{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}\wedge \forall {x}\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}\phantom{\rule{.4em}{0ex}}{T}\left({x}{\cdot }_{{C}}{y}\right)={T}\left({x}\right){\cdot }_{{Q}}{T}\left({y}\right)\wedge {T}\left({1}_{{C}}\right)={1}_{{Q}}\right)$
28 eqid ${⊢}{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}$
29 eqid ${⊢}{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}$
30 eqid ${⊢}{\cdot }_{{C}}={\cdot }_{{C}}$
31 7 30 mgpplusg ${⊢}{\cdot }_{{C}}={+}_{{\mathrm{mulGrp}}_{{C}}}$
32 eqid ${⊢}{\cdot }_{{Q}}={\cdot }_{{Q}}$
33 12 32 mgpplusg ${⊢}{\cdot }_{{Q}}={+}_{{\mathrm{mulGrp}}_{{Q}}}$
34 eqid ${⊢}{1}_{{C}}={1}_{{C}}$
35 7 34 ringidval ${⊢}{1}_{{C}}={0}_{{\mathrm{mulGrp}}_{{C}}}$
36 eqid ${⊢}{1}_{{Q}}={1}_{{Q}}$
37 12 36 ringidval ${⊢}{1}_{{Q}}={0}_{{\mathrm{mulGrp}}_{{Q}}}$
38 28 29 31 33 35 37 ismhm ${⊢}{T}\in \left({\mathrm{mulGrp}}_{{C}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{Q}}\right)↔\left(\left({\mathrm{mulGrp}}_{{C}}\in \mathrm{Mnd}\wedge {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}\right)\wedge \left({T}:{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}⟶{\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}\wedge \forall {x}\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{C}}}\phantom{\rule{.4em}{0ex}}{T}\left({x}{\cdot }_{{C}}{y}\right)={T}\left({x}\right){\cdot }_{{Q}}{T}\left({y}\right)\wedge {T}\left({1}_{{C}}\right)={1}_{{Q}}\right)\right)$
39 9 14 27 38 syl21anbrc ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({\mathrm{mulGrp}}_{{C}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{Q}}\right)$