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=Poly1R
pm2mpfo.c C=NMatP
pm2mpfo.b B=BaseC
pm2mpfo.m ˙=Q
pm2mpfo.e ×˙=mulGrpQ
pm2mpfo.x X=var1A
pm2mpfo.a A=NMatR
pm2mpfo.q Q=Poly1A
pm2mpfo.l L=BaseQ
pm2mpfo.t T=NpMatToMatPolyR
Assertion pm2mpgrpiso NFinRRingTCGrpIsoQ

Proof

Step Hyp Ref Expression
1 pm2mpfo.p P=Poly1R
2 pm2mpfo.c C=NMatP
3 pm2mpfo.b B=BaseC
4 pm2mpfo.m ˙=Q
5 pm2mpfo.e ×˙=mulGrpQ
6 pm2mpfo.x X=var1A
7 pm2mpfo.a A=NMatR
8 pm2mpfo.q Q=Poly1A
9 pm2mpfo.l L=BaseQ
10 pm2mpfo.t T=NpMatToMatPolyR
11 1 2 3 4 5 6 7 8 9 10 pm2mpghm NFinRRingTCGrpHomQ
12 eqid BaseQ=BaseQ
13 1 2 3 4 5 6 7 8 12 10 pm2mpf1o NFinRRingT:B1-1 ontoBaseQ
14 3 12 isgim TCGrpIsoQTCGrpHomQT:B1-1 ontoBaseQ
15 11 13 14 sylanbrc NFinRRingTCGrpIsoQ