mat1ric

Description: A ring is isomorphic to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 30-Dec-2019)

		Ref	Expression
	Hypothesis	mat1ric.a	$⊢ A = \{E\} Mat R$
	Assertion	mat1ric	$⊢ (R \in Ring \land E \in V) \to R ≃_{𝑟} A$

Step	Hyp	Ref	Expression
1		mat1ric.a	$⊢ A = \{E\} Mat R$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ {Base}_{A} = {Base}_{A}$
4		eqid	$⊢ ⟨E, E⟩ = ⟨E, E⟩$
5		opeq2	$⊢ x = y \to ⟨⟨E, E⟩, x⟩ = ⟨⟨E, E⟩, y⟩$
6	5	sneqd	$⊢ x = y \to \{⟨⟨E, E⟩, x⟩\} = \{⟨⟨E, E⟩, y⟩\}$
7	6	cbvmptv	$⊢ (x \in {Base}_{R} ⟼ \{⟨⟨E, E⟩, x⟩\}) = (y \in {Base}_{R} ⟼ \{⟨⟨E, E⟩, y⟩\})$
8	2 1 3 4 7	mat1rngiso	$⊢ (R \in Ring \land E \in V) \to (x \in {Base}_{R} ⟼ \{⟨⟨E, E⟩, x⟩\}) \in (R RingIso A)$
9	8	ne0d	$⊢ (R \in Ring \land E \in V) \to R RingIso A \neq \emptyset$
10		brric	$⊢ R ≃_{𝑟} A \leftrightarrow R RingIso A \neq \emptyset$
11	9 10	sylibr	$⊢ (R \in Ring \land E \in V) \to R ≃_{𝑟} A$

Metamath Proof Explorer