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