Metamath Proof Explorer

Theorem tdrgtrg

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

		Ref	Expression
	Assertion	tdrgtrg	$⊢ R \in TopDRing \to R \in TopRing$

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	simp1bi	$⊢ R \in TopDRing \to R \in TopRing$