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 = N Mat R$
		matcpmric.p	$⊢ P = {Poly}_{1} (R)$
		matcpmric.c	$⊢ C = N Mat P$
		matcpmric.s	$⊢ S = N ConstPolyMat R$
		matcpmric.u	$⊢ U = C ↾_{𝑠} S$
	Assertion	matcpmric	$⊢ (N \in Fin \land R \in CRing) \to A ≃_{𝑟} U$

Proof

Step	Hyp	Ref	Expression
1		matcpmric.a	$⊢ A = N Mat R$
2		matcpmric.p	$⊢ P = {Poly}_{1} (R)$
3		matcpmric.c	$⊢ C = N Mat P$
4		matcpmric.s	$⊢ S = N ConstPolyMat R$
5		matcpmric.u	$⊢ U = C ↾_{𝑠} 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 \in Fin \land R \in CRing) \to N matToPolyMat R \in (A RingIso U)$
9	8	ne0d	$⊢ (N \in Fin \land R \in CRing) \to A RingIso U \neq \emptyset$
10		brric	$⊢ A ≃_{𝑟} U \leftrightarrow A RingIso U \neq \emptyset$
11	9 10	sylibr	$⊢ (N \in Fin \land R \in CRing) \to A ≃_{𝑟} U$