Theorem islvec

Description: The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013)

	Ref	Expression
Hypothesis	islvec.1	|- F = ( Scalar ` W )
Assertion	islvec	|- ( W e. LVec <-> ( W e. LMod /\ F e. DivRing ) )

Proof

Step	Hyp	Ref	Expression
1		islvec.1	|- F = ( Scalar ` W )
2		fveq2	|- ( f = W -> ( Scalar ` f ) = ( Scalar ` W ) )
3	2 1	eqtr4di	|- ( f = W -> ( Scalar ` f ) = F )
4	3	eleq1d	|- ( f = W -> ( ( Scalar ` f ) e. DivRing <-> F e. DivRing ) )
5		df-lvec	|- LVec = { f e. LMod | ( Scalar ` f ) e. DivRing }
6	4 5	elrab2	|- ( W e. LVec <-> ( W e. LMod /\ F e. DivRing ) )