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 = ( N Mat R )
	matcpmric.p	|- P = ( Poly1 ` R )
	matcpmric.c	|- C = ( N Mat P )
	matcpmric.s	|- S = ( N ConstPolyMat R )
	matcpmric.u	|- U = ( C |`s S )
Assertion	matcpmric	|- ( ( N e. Fin /\ R e. CRing ) -> A ~=r U )

Proof

Step	Hyp	Ref	Expression
1		matcpmric.a	|- A = ( N Mat R )
2		matcpmric.p	|- P = ( Poly1 ` R )
3		matcpmric.c	|- C = ( N Mat P )
4		matcpmric.s	|- S = ( N ConstPolyMat R )
5		matcpmric.u	|- U = ( C |`s S )
6		eqid	|- ( N matToPolyMat R ) = ( N matToPolyMat R )
7		eqid	|- ( Base ` A ) = ( Base ` A )
8	4 6 1 7 2 3 5	m2cpmrngiso	|- ( ( N e. Fin /\ R e. CRing ) -> ( N matToPolyMat R ) e. ( A RingIso U ) )
9	8	ne0d	|- ( ( N e. Fin /\ R e. CRing ) -> ( A RingIso U ) =/= (/) )
10		brric	|- ( A ~=r U <-> ( A RingIso U ) =/= (/) )
11	9 10	sylibr	|- ( ( N e. Fin /\ R e. CRing ) -> A ~=r U )