Theorem tdrgtrg

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

	Ref	Expression
Assertion	tdrgtrg	⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ TopRing )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
2		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
3	1 2	istdrg	⊢ ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) ) ∈ TopGrp ) )
4	3	simp1bi	⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ TopRing )