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	|- M = ( mulGrp ` R )
	istdrg.1	|- U = ( Unit ` R )
Assertion	tdrgunit	|- ( R e. TopDRing -> ( M |`s U ) e. TopGrp )

Proof

Step	Hyp	Ref	Expression
1		istrg.1	|- M = ( mulGrp ` R )
2		istdrg.1	|- U = ( Unit ` R )
3	1 2	istdrg	|- ( R e. TopDRing <-> ( R e. TopRing /\ R e. DivRing /\ ( M |`s U ) e. TopGrp ) )
4	3	simp3bi	|- ( R e. TopDRing -> ( M |`s U ) e. TopGrp )