Metamath Proof Explorer


Theorem istrg

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

Ref Expression
Hypothesis istrg.1
|- M = ( mulGrp ` R )
Assertion istrg
|- ( R e. TopRing <-> ( R e. TopGrp /\ R e. Ring /\ M e. TopMnd ) )

Proof

Step Hyp Ref Expression
1 istrg.1
 |-  M = ( mulGrp ` R )
2 elin
 |-  ( R e. ( TopGrp i^i Ring ) <-> ( R e. TopGrp /\ R e. Ring ) )
3 2 anbi1i
 |-  ( ( R e. ( TopGrp i^i Ring ) /\ M e. TopMnd ) <-> ( ( R e. TopGrp /\ R e. Ring ) /\ M e. TopMnd ) )
4 fveq2
 |-  ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
5 4 1 eqtr4di
 |-  ( r = R -> ( mulGrp ` r ) = M )
6 5 eleq1d
 |-  ( r = R -> ( ( mulGrp ` r ) e. TopMnd <-> M e. TopMnd ) )
7 df-trg
 |-  TopRing = { r e. ( TopGrp i^i Ring ) | ( mulGrp ` r ) e. TopMnd }
8 6 7 elrab2
 |-  ( R e. TopRing <-> ( R e. ( TopGrp i^i Ring ) /\ M e. TopMnd ) )
9 df-3an
 |-  ( ( R e. TopGrp /\ R e. Ring /\ M e. TopMnd ) <-> ( ( R e. TopGrp /\ R e. Ring ) /\ M e. TopMnd ) )
10 3 8 9 3bitr4i
 |-  ( R e. TopRing <-> ( R e. TopGrp /\ R e. Ring /\ M e. TopMnd ) )