Database
BASIC TOPOLOGY
Filters and filter bases
Topological rings, fields, vector spaces
trgtps
Next ⟩
trgring
Metamath Proof Explorer
Ascii
Unicode
Theorem
trgtps
Description:
A topological ring is a topological space.
(Contributed by
Mario Carneiro
, 5-Oct-2015)
Ref
Expression
Assertion
trgtps
⊢
R
∈
TopRing
→
R
∈
TopSp
Proof
Step
Hyp
Ref
Expression
1
trgtgp
⊢
R
∈
TopRing
→
R
∈
TopGrp
2
tgptps
⊢
R
∈
TopGrp
→
R
∈
TopSp
3
1
2
syl
⊢
R
∈
TopRing
→
R
∈
TopSp