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 = { 𝑟 ∈ ( TopGrp ∩ Ring ) ∣ ( mulGrp ‘ 𝑟 ) ∈ TopMnd }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrg TopRing
1 vr 𝑟
2 ctgp TopGrp
3 crg Ring
4 2 3 cin ( TopGrp ∩ Ring )
5 cmgp mulGrp
6 1 cv 𝑟
7 6 5 cfv ( mulGrp ‘ 𝑟 )
8 ctmd TopMnd
9 7 8 wcel ( mulGrp ‘ 𝑟 ) ∈ TopMnd
10 9 1 4 crab { 𝑟 ∈ ( TopGrp ∩ Ring ) ∣ ( mulGrp ‘ 𝑟 ) ∈ TopMnd }
11 0 10 wceq TopRing = { 𝑟 ∈ ( TopGrp ∩ Ring ) ∣ ( mulGrp ‘ 𝑟 ) ∈ TopMnd }