Database
BASIC TOPOLOGY
Filters and filter bases
Topological rings, fields, vector spaces
df-trg
Metamath Proof Explorer
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 }