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 = { 𝑤 ∈ 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 }