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-tvc
Description: Define a topological left vector space, which is a topological module over
a topological division ring. (Contributed by Mario Carneiro , 5-Oct-2015)
Ref
Expression
Assertion
df-tvc ⊢ TopVec = { 𝑤 ∈ TopMod ∣ ( Scalar ‘ 𝑤 ) ∈ TopDRing }
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
ctvc ⊢ TopVec
1
vw ⊢ 𝑤
2
ctlm ⊢ TopMod
3
csca ⊢ Scalar
4
1
cv ⊢ 𝑤
5
4 3
cfv ⊢ ( Scalar ‘ 𝑤 )
6
ctdrg ⊢ TopDRing
7
5 6
wcel ⊢ ( Scalar ‘ 𝑤 ) ∈ TopDRing
8
7 1 2
crab ⊢ { 𝑤 ∈ TopMod ∣ ( Scalar ‘ 𝑤 ) ∈ TopDRing }
9
0 8
wceq ⊢ TopVec = { 𝑤 ∈ TopMod ∣ ( Scalar ‘ 𝑤 ) ∈ TopDRing }