Description: A topological division ring is a division ring. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | tdrgdrng | |- ( R e. TopDRing -> R e. DivRing ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |- ( mulGrp ` R ) = ( mulGrp ` R ) |
|
2 | eqid | |- ( Unit ` R ) = ( Unit ` R ) |
|
3 | 1 2 | istdrg | |- ( R e. TopDRing <-> ( R e. TopRing /\ R e. DivRing /\ ( ( mulGrp ` R ) |`s ( Unit ` R ) ) e. TopGrp ) ) |
4 | 3 | simp2bi | |- ( R e. TopDRing -> R e. DivRing ) |