Theorem 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=\left\{E\right\}\mathrm{Mat}R$$
Assertion	mat1ric	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\right)\to R{\simeq }_{𝑟}A$$

Proof

Step	Hyp	Ref	Expression
1		mat1ric.a	$$⊢A=\left\{E\right\}\mathrm{Mat}R$$
2		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
3		eqid	$$⊢{\mathrm{Base}}_A={\mathrm{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 \left\{⟨⟨E,E⟩,x⟩\right\}=\left\{⟨⟨E,E⟩,y⟩\right\}$$
7	6	cbvmptv	$$⊢\left(x\in {\mathrm{Base}}_R⟼\left\{⟨⟨E,E⟩,x⟩\right\}\right)=\left(y\in {\mathrm{Base}}_R⟼\left\{⟨⟨E,E⟩,y⟩\right\}\right)$$
8	2 1 3 4 7	mat1rngiso	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\right)\to \left(x\in {\mathrm{Base}}_R⟼\left\{⟨⟨E,E⟩,x⟩\right\}\right)\in \left(R\mathrm{RingIso}A\right)$$
9	8	ne0d	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\right)\to R\mathrm{RingIso}A\ne \varnothing$$
10		brric	$$⊢R{\simeq }_{𝑟}A\leftrightarrow R\mathrm{RingIso}A\ne \varnothing$$
11	9 10	sylibr	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\right)\to R{\simeq }_{𝑟}A$$