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 = { w e. TopMod | ( Scalar ` w ) e. TopDRing }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctvc	|- TopVec
1		vw	|- w
2		ctlm	|- TopMod
3		csca	|- Scalar
4	1	cv	|- w
5	4 3	cfv	|- ( Scalar ` w )
6		ctdrg	|- TopDRing
7	5 6	wcel	|- ( Scalar ` w ) e. TopDRing
8	7 1 2	crab	|- { w e. TopMod | ( Scalar ` w ) e. TopDRing }
9	0 8	wceq	|- TopVec = { w e. TopMod | ( Scalar ` w ) e. TopDRing }