Metamath Proof Explorer

Theorem trgtgp

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

		Ref	Expression
	Assertion	trgtgp	$⊢ R \in TopRing \to R \in TopGrp$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
2	1	istrg	$⊢ R \in TopRing \leftrightarrow (R \in TopGrp \land R \in Ring \land {mulGrp}_{R} \in TopMnd)$
3	2	simp1bi	$⊢ R \in TopRing \to R \in TopGrp$