Metamath Proof Explorer

Theorem istdrg2

Description: A topological-ring division ring is a topological division ring iff the group of nonzero elements is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses istdrg2.m 
|- M = ( mulGrp ` R )
istdrg2.b 
|- B = ( Base ` R )
istdrg2.z 
|- .0. = ( 0g ` R )
Assertion istdrg2 
|- ( R e. TopDRing <-> ( R e. TopRing /\ R e. DivRing /\ ( M |`s ( B \ { .0. } ) ) e. TopGrp ) )

Proof

Step Hyp Ref Expression
1 istdrg2.m 
 |-  M = ( mulGrp ` R )
2 istdrg2.b 
 |-  B = ( Base ` R )
3 istdrg2.z 
 |-  .0. = ( 0g ` R )
4 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
5 1 4 istdrg 
 |-  ( R e. TopDRing <-> ( R e. TopRing /\ R e. DivRing /\ ( M |`s ( Unit ` R ) ) e. TopGrp ) )
6 2 4 3 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) )
7 6 simprbi 
 |-  ( R e. DivRing -> ( Unit ` R ) = ( B \ { .0. } ) )
8 7 adantl 
 |-  ( ( R e. TopRing /\ R e. DivRing ) -> ( Unit ` R ) = ( B \ { .0. } ) )
9 8 oveq2d 
 |-  ( ( R e. TopRing /\ R e. DivRing ) -> ( M |`s ( Unit ` R ) ) = ( M |`s ( B \ { .0. } ) ) )
10 9 eleq1d 
 |-  ( ( R e. TopRing /\ R e. DivRing ) -> ( ( M |`s ( Unit ` R ) ) e. TopGrp <-> ( M |`s ( B \ { .0. } ) ) e. TopGrp ) )
11 10 pm5.32i 
 |-  ( ( ( R e. TopRing /\ R e. DivRing ) /\ ( M |`s ( Unit ` R ) ) e. TopGrp ) <-> ( ( R e. TopRing /\ R e. DivRing ) /\ ( M |`s ( B \ { .0. } ) ) e. TopGrp ) )
12 df-3an 
 |-  ( ( R e. TopRing /\ R e. DivRing /\ ( M |`s ( Unit ` R ) ) e. TopGrp ) <-> ( ( R e. TopRing /\ R e. DivRing ) /\ ( M |`s ( Unit ` R ) ) e. TopGrp ) )
13 df-3an 
 |-  ( ( R e. TopRing /\ R e. DivRing /\ ( M |`s ( B \ { .0. } ) ) e. TopGrp ) <-> ( ( R e. TopRing /\ R e. DivRing ) /\ ( M |`s ( B \ { .0. } ) ) e. TopGrp ) )
14 11 12 13 3bitr4i 
 |-  ( ( R e. TopRing /\ R e. DivRing /\ ( M |`s ( Unit ` R ) ) e. TopGrp ) <-> ( R e. TopRing /\ R e. DivRing /\ ( M |`s ( B \ { .0. } ) ) e. TopGrp ) )
15 5 14 bitri 
 |-  ( R e. TopDRing <-> ( R e. TopRing /\ R e. DivRing /\ ( M |`s ( B \ { .0. } ) ) e. TopGrp ) )