Metamath Proof Explorer


Theorem matcpmric

Description: The ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring. (Contributed by AV, 30-Dec-2019)

Ref Expression
Hypotheses matcpmric.a A=NMatR
matcpmric.p P=Poly1R
matcpmric.c C=NMatP
matcpmric.s S=NConstPolyMatR
matcpmric.u U=C𝑠S
Assertion matcpmric NFinRCRingA𝑟U

Proof

Step Hyp Ref Expression
1 matcpmric.a A=NMatR
2 matcpmric.p P=Poly1R
3 matcpmric.c C=NMatP
4 matcpmric.s S=NConstPolyMatR
5 matcpmric.u U=C𝑠S
6 eqid NmatToPolyMatR=NmatToPolyMatR
7 eqid BaseA=BaseA
8 4 6 1 7 2 3 5 m2cpmrngiso NFinRCRingNmatToPolyMatRARingIsoU
9 8 ne0d NFinRCRingARingIsoU
10 brric A𝑟UARingIsoU
11 9 10 sylibr NFinRCRingA𝑟U