mat1rngiso

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

	Ref	Expression
Hypotheses	mat1rhmval.k	$⊢ K = {Base}_{R}$
	mat1rhmval.a	$⊢ A = \{E\} Mat R$
	mat1rhmval.b	$⊢ B = {Base}_{A}$
	mat1rhmval.o	$⊢ O = ⟨E, E⟩$
	mat1rhmval.f	$⊢ F = (x \in K ⟼ \{⟨O, x⟩\})$
Assertion	mat1rngiso	$⊢ (R \in Ring \land E \in V) \to F \in (R RingIso A)$

Step	Hyp	Ref	Expression
1		mat1rhmval.k	$⊢ K = {Base}_{R}$
2		mat1rhmval.a	$⊢ A = \{E\} Mat R$
3		mat1rhmval.b	$⊢ B = {Base}_{A}$
4		mat1rhmval.o	$⊢ O = ⟨E, E⟩$
5		mat1rhmval.f	$⊢ F = (x \in K ⟼ \{⟨O, x⟩\})$
6	1 2 3 4 5	mat1rhm	$⊢ (R \in Ring \land E \in V) \to F \in (R RingHom A)$
7	1 2 3 4 5	mat1f1o	$⊢ (R \in Ring \land E \in V) \to F : K \underset{1-1 onto}{⟶} B$
8	1 3	isrim	$⊢ F \in (R RingIso A) \leftrightarrow (F \in (R RingHom A) \land F : K \underset{1-1 onto}{⟶} B)$
9	6 7 8	sylanbrc	$⊢ (R \in Ring \land E \in V) \to F \in (R RingIso A)$

Metamath Proof Explorer