drngdomn

Description: A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015)

		Ref	Expression
	Assertion	drngdomn	$⊢ R \in DivRing \to R \in Domn$

Step	Hyp	Ref	Expression
1		drngnzr	$⊢ R \in DivRing \to R \in NzRing$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ Unit (R) = Unit (R)$
4		eqid	$⊢ 0_{R} = 0_{R}$
5	2 3 4	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = {Base}_{R} ∖ \{0_{R}\})$
6	5	simprbi	$⊢ R \in DivRing \to Unit (R) = {Base}_{R} ∖ \{0_{R}\}$
7		drngring	$⊢ R \in DivRing \to R \in Ring$
8		eqid	$⊢ RLReg (R) = RLReg (R)$
9	8 3	unitrrg	$⊢ R \in Ring \to Unit (R) \subseteq RLReg (R)$
10	7 9	syl	$⊢ R \in DivRing \to Unit (R) \subseteq RLReg (R)$
11	6 10	eqsstrrd	$⊢ R \in DivRing \to {Base}_{R} ∖ \{0_{R}\} \subseteq RLReg (R)$
12	2 8 4	isdomn2	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land {Base}_{R} ∖ \{0_{R}\} \subseteq RLReg (R))$
13	1 11 12	sylanbrc	$⊢ R \in DivRing \to R \in Domn$

Metamath Proof Explorer