Metamath Proof Explorer


Definition 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=wTopMod|ScalarwTopDRing

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctvc classTopVec
1 vw setvarw
2 ctlm classTopMod
3 csca classScalar
4 1 cv setvarw
5 4 3 cfv classScalarw
6 ctdrg classTopDRing
7 5 6 wcel wffScalarwTopDRing
8 7 1 2 crab classwTopMod|ScalarwTopDRing
9 0 8 wceq wffTopVec=wTopMod|ScalarwTopDRing