Theorem drngring

Description: A division ring is a ring. (Contributed by NM, 8-Sep-2011)

	Ref	Expression
Assertion	drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
3		eqid	$$⊢0_R=0_R$$
4	1 2 3	isdrng	$$⊢R\in \mathrm{DivRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge \mathrm{Unit}\left(R\right)={\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)$$
5	4	simplbi	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$