scmatric

Description: A ring is isomorphic to every ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019)

	Ref	Expression
Hypotheses	scmatric.a	$⊢ A = N Mat R$
	scmatric.c	$⊢ C = N ScMat R$
	scmatric.s	$⊢ S = A ↾_{𝑠} C$
Assertion	scmatric	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to R ≃_{𝑟} S$

Step	Hyp	Ref	Expression
1		scmatric.a	$⊢ A = N Mat R$
2		scmatric.c	$⊢ C = N ScMat R$
3		scmatric.s	$⊢ S = A ↾_{𝑠} C$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ 1_{A} = 1_{A}$
6		eqid	$⊢ \cdot_{A} = \cdot_{A}$
7		eqid	$⊢ (x \in {Base}_{R} ⟼ x \cdot_{A} 1_{A}) = (x \in {Base}_{R} ⟼ x \cdot_{A} 1_{A})$
8	4 1 5 6 7 2 3	scmatrngiso	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to (x \in {Base}_{R} ⟼ x \cdot_{A} 1_{A}) \in (R RingIso S)$
9	8	ne0d	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to R RingIso S \neq \emptyset$
10		brric	$⊢ R ≃_{𝑟} S \leftrightarrow R RingIso S \neq \emptyset$
11	9 10	sylibr	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to R ≃_{𝑟} S$

Metamath Proof Explorer