Metamath Proof Explorer


Theorem m2cpmmhm

Description: The transformation of matrices into constant polynomial matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses m2cpm.s S=NConstPolyMatR
m2cpm.t T=NmatToPolyMatR
m2cpm.a A=NMatR
m2cpm.b B=BaseA
m2cpmghm.p P=Poly1R
m2cpmghm.c C=NMatP
m2cpmghm.u U=C𝑠S
Assertion m2cpmmhm NFinRCRingTmulGrpAMndHommulGrpU

Proof

Step Hyp Ref Expression
1 m2cpm.s S=NConstPolyMatR
2 m2cpm.t T=NmatToPolyMatR
3 m2cpm.a A=NMatR
4 m2cpm.b B=BaseA
5 m2cpmghm.p P=Poly1R
6 m2cpmghm.c C=NMatP
7 m2cpmghm.u U=C𝑠S
8 eqid BaseC=BaseC
9 2 3 4 5 6 8 mat2pmatmhm NFinRCRingTmulGrpAMndHommulGrpC
10 crngring RCRingRRing
11 10 anim2i NFinRCRingNFinRRing
12 1 5 6 cpmatsrgpmat NFinRRingSSubRingC
13 eqid mulGrpC=mulGrpC
14 13 subrgsubm SSubRingCSSubMndmulGrpC
15 11 12 14 3syl NFinRCRingSSubMndmulGrpC
16 1 2 3 4 m2cpmf NFinRRingT:BS
17 frn T:BSranTS
18 11 16 17 3syl NFinRCRingranTS
19 6 ovexi CV
20 1 ovexi SV
21 7 13 mgpress CVSVmulGrpC𝑠S=mulGrpU
22 19 20 21 mp2an mulGrpC𝑠S=mulGrpU
23 22 eqcomi mulGrpU=mulGrpC𝑠S
24 23 resmhm2b SSubMndmulGrpCranTSTmulGrpAMndHommulGrpCTmulGrpAMndHommulGrpU
25 15 18 24 syl2anc NFinRCRingTmulGrpAMndHommulGrpCTmulGrpAMndHommulGrpU
26 9 25 mpbid NFinRCRingTmulGrpAMndHommulGrpU