Theorem trgtgp

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

	Ref	Expression
Assertion	trgtgp	⊢ ( 𝑅 ∈ TopRing → 𝑅 ∈ TopGrp )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
2	1	istrg	⊢ ( 𝑅 ∈ TopRing ↔ ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ ( mulGrp ‘ 𝑅 ) ∈ TopMnd ) )
3	2	simp1bi	⊢ ( 𝑅 ∈ TopRing → 𝑅 ∈ TopGrp )