Metamath Proof Explorer

Theorem tdrgdrng

Description: A topological division ring is a division ring. (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Assertion	tdrgdrng	$⊢ R \in TopDRing \to R \in DivRing$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
2		eqid	$⊢ Unit (R) = Unit (R)$
3	1 2	istdrg	$⊢ R \in TopDRing \leftrightarrow (R \in TopRing \land R \in DivRing \land {mulGrp}_{R} ↾_{𝑠} Unit (R) \in TopGrp)$
4	3	simp2bi	$⊢ R \in TopDRing \to R \in DivRing$