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	$$⊢\mathrm{TopVec}=\left\{w\in \mathrm{TopMod}|\mathrm{Scalar}\left(w\right)\in \mathrm{TopDRing}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctvc	$$class\mathrm{TopVec}$$
1		vw	$$setvarw$$
2		ctlm	$$class\mathrm{TopMod}$$
3		csca	$$class\mathrm{Scalar}$$
4	1	cv	$$setvarw$$
5	4 3	cfv	$$class\mathrm{Scalar}\left(w\right)$$
6		ctdrg	$$class\mathrm{TopDRing}$$
7	5 6	wcel	$$wff\mathrm{Scalar}\left(w\right)\in \mathrm{TopDRing}$$
8	7 1 2	crab	$$class\left\{w\in \mathrm{TopMod}|\mathrm{Scalar}\left(w\right)\in \mathrm{TopDRing}\right\}$$
9	0 8	wceq	$$wff\mathrm{TopVec}=\left\{w\in \mathrm{TopMod}|\mathrm{Scalar}\left(w\right)\in \mathrm{TopDRing}\right\}$$