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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matcpmric.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	matcpmric.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	matcpmric.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	matcpmric.u	⊢ 𝑈 = ( 𝐶 ↾s 𝑆 )
Assertion	matcpmric	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ≃𝑟 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		matcpmric.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matcpmric.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		matcpmric.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
4		matcpmric.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
5		matcpmric.u	⊢ 𝑈 = ( 𝐶 ↾s 𝑆 )
6		eqid	⊢ ( 𝑁 matToPolyMat 𝑅 ) = ( 𝑁 matToPolyMat 𝑅 )
7		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
8	4 6 1 7 2 3 5	m2cpmrngiso	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 matToPolyMat 𝑅 ) ∈ ( 𝐴 RingIso 𝑈 ) )
9	8	ne0d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝐴 RingIso 𝑈 ) ≠ ∅ )
10		brric	⊢ ( 𝐴 ≃𝑟 𝑈 ↔ ( 𝐴 RingIso 𝑈 ) ≠ ∅ )
11	9 10	sylibr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ≃𝑟 𝑈 )