Metamath Proof Explorer


Definition df-trg

Description: Define a topological ring, which is a ring such that the addition is a topological group operation and the multiplication is continuous. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion df-trg
|- TopRing = { r e. ( TopGrp i^i Ring ) | ( mulGrp ` r ) e. TopMnd }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrg
 |-  TopRing
1 vr
 |-  r
2 ctgp
 |-  TopGrp
3 crg
 |-  Ring
4 2 3 cin
 |-  ( TopGrp i^i Ring )
5 cmgp
 |-  mulGrp
6 1 cv
 |-  r
7 6 5 cfv
 |-  ( mulGrp ` r )
8 ctmd
 |-  TopMnd
9 7 8 wcel
 |-  ( mulGrp ` r ) e. TopMnd
10 9 1 4 crab
 |-  { r e. ( TopGrp i^i Ring ) | ( mulGrp ` r ) e. TopMnd }
11 0 10 wceq
 |-  TopRing = { r e. ( TopGrp i^i Ring ) | ( mulGrp ` r ) e. TopMnd }