Theorem tdrgunit

Description: The unit group of a topological division ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	istrg.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	istdrg.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	tdrgunit	⊢ ( 𝑅 ∈ TopDRing → ( 𝑀 ↾s 𝑈 ) ∈ TopGrp )

Proof

Step	Hyp	Ref	Expression
1		istrg.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		istdrg.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3	1 2	istdrg	⊢ ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) )
4	3	simp3bi	⊢ ( 𝑅 ∈ TopDRing → ( 𝑀 ↾s 𝑈 ) ∈ TopGrp )