This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )