Theorem istvc

Description: A topological vector space is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypothesis	tlmtrg.f	|- F = ( Scalar ` W )
Assertion	istvc	|- ( W e. TopVec <-> ( W e. TopMod /\ F e. TopDRing ) )

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	|- F = ( Scalar ` W )
2		fveq2	|- ( x = W -> ( Scalar ` x ) = ( Scalar ` W ) )
3	2 1	eqtr4di	|- ( x = W -> ( Scalar ` x ) = F )
4	3	eleq1d	|- ( x = W -> ( ( Scalar ` x ) e. TopDRing <-> F e. TopDRing ) )
5		df-tvc	|- TopVec = { x e. TopMod | ( Scalar ` x ) e. TopDRing }
6	4 5	elrab2	|- ( W e. TopVec <-> ( W e. TopMod /\ F e. TopDRing ) )