This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Filters and filter bases Topological rings, fields, vector spaces 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 }