Theorem tdrgdrng

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

	Ref	Expression
Assertion	tdrgdrng	⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ DivRing )

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	simp2bi	⊢ ( 𝑅 ∈ TopDRing → 𝑅 ∈ DivRing )