Metamath Proof Explorer

Theorem istdrg

Description: Express the predicate " R is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses istrg.1 
|- M = ( mulGrp ` R )
istdrg.1 
|- U = ( Unit ` R )
Assertion istdrg 
|- ( R e. TopDRing <-> ( R e. TopRing /\ R e. DivRing /\ ( M |`s U ) e. TopGrp ) )

Proof

Step Hyp Ref Expression
1 istrg.1 
 |-  M = ( mulGrp ` R )
2 istdrg.1 
 |-  U = ( Unit ` R )
3 elin 
 |-  ( R e. ( TopRing i^i DivRing ) <-> ( R e. TopRing /\ R e. DivRing ) )
4 3 anbi1i 
 |-  ( ( R e. ( TopRing i^i DivRing ) /\ ( M |`s U ) e. TopGrp ) <-> ( ( R e. TopRing /\ R e. DivRing ) /\ ( M |`s U ) e. TopGrp ) )
5 fveq2 
 |-  ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
6 5 1 eqtr4di 
 |-  ( r = R -> ( mulGrp ` r ) = M )
7 fveq2 
 |-  ( r = R -> ( Unit ` r ) = ( Unit ` R ) )
8 7 2 eqtr4di 
 |-  ( r = R -> ( Unit ` r ) = U )
9 6 8 oveq12d 
 |-  ( r = R -> ( ( mulGrp ` r ) |`s ( Unit ` r ) ) = ( M |`s U ) )
10 9 eleq1d 
 |-  ( r = R -> ( ( ( mulGrp ` r ) |`s ( Unit ` r ) ) e. TopGrp <-> ( M |`s U ) e. TopGrp ) )
11 df-tdrg 
 |-  TopDRing = { r e. ( TopRing i^i DivRing ) | ( ( mulGrp ` r ) |`s ( Unit ` r ) ) e. TopGrp }
12 10 11 elrab2 
 |-  ( R e. TopDRing <-> ( R e. ( TopRing i^i DivRing ) /\ ( M |`s U ) e. TopGrp ) )
13 df-3an 
 |-  ( ( R e. TopRing /\ R e. DivRing /\ ( M |`s U ) e. TopGrp ) <-> ( ( R e. TopRing /\ R e. DivRing ) /\ ( M |`s U ) e. TopGrp ) )
14 4 12 13 3bitr4i 
 |-  ( R e. TopDRing <-> ( R e. TopRing /\ R e. DivRing /\ ( M |`s U ) e. TopGrp ) )