Metamath Proof Explorer

Theorem scmatrngiso

Description: There is a ring isomorphism from a ring to the ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019)

		Ref	Expression
	Hypotheses	scmatrhmval.k	$⊢ K = {Base}_{R}$
		scmatrhmval.a	$⊢ A = N Mat R$
		scmatrhmval.o	$⊢ \underset{˙}{1} = 1_{A}$
		scmatrhmval.t	$⊢ \underset{˙}{*} = \cdot_{A}$
		scmatrhmval.f	$⊢ F = (x \in K ⟼ x \underset{˙}{*} \underset{˙}{1})$
		scmatrhmval.c	$⊢ C = N ScMat R$
		scmatghm.s	$⊢ S = A ↾_{𝑠} C$
	Assertion	scmatrngiso	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to F \in (R RingIso S)$

Proof

Step	Hyp	Ref	Expression
1		scmatrhmval.k	$⊢ K = {Base}_{R}$
2		scmatrhmval.a	$⊢ A = N Mat R$
3		scmatrhmval.o	$⊢ \underset{˙}{1} = 1_{A}$
4		scmatrhmval.t	$⊢ \underset{˙}{*} = \cdot_{A}$
5		scmatrhmval.f	$⊢ F = (x \in K ⟼ x \underset{˙}{*} \underset{˙}{1})$
6		scmatrhmval.c	$⊢ C = N ScMat R$
7		scmatghm.s	$⊢ S = A ↾_{𝑠} C$
8	1 2 3 4 5 6 7	scmatrhm	$⊢ (N \in Fin \land R \in Ring) \to F \in (R RingHom S)$
9	8	3adant2	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to F \in (R RingHom S)$
10	1 2 3 4 5 6	scmatf1o	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to F : K \underset{1-1 onto}{⟶} C$
11	2 6 7	scmatstrbas	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{S} = C$
12	11	3adant2	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to {Base}_{S} = C$
13	12	f1oeq3d	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to (F : K \underset{1-1 onto}{⟶} {Base}_{S} \leftrightarrow F : K \underset{1-1 onto}{⟶} C)$
14	10 13	mpbird	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to F : K \underset{1-1 onto}{⟶} {Base}_{S}$
15		eqid	$⊢ {Base}_{S} = {Base}_{S}$
16	1 15	isrim	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F : K \underset{1-1 onto}{⟶} {Base}_{S})$
17	9 14 16	sylanbrc	$⊢ (N \in Fin \land N \neq \emptyset \land R \in Ring) \to F \in (R RingIso S)$