This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem drngring

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

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

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ Unit (R) = Unit (R)$
3		eqid	$⊢ 0_{R} = 0_{R}$
4	1 2 3	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = {Base}_{R} ∖ \{0_{R}\})$
5	4	simplbi	$⊢ R \in DivRing \to R \in Ring$