Metamath Proof Explorer

Theorem trgring

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

		Ref	Expression
	Assertion	trgring	$⊢ R \in TopRing \to R \in Ring$

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	simp2bi	$⊢ R \in TopRing \to R \in Ring$