Metamath Proof Explorer


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 )