Theorem islvec

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

	Ref	Expression
Hypothesis	islvec.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	islvec	⊢ ( 𝑊 ∈ LVec ↔ ( 𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing ) )

Proof

Step	Hyp	Ref	Expression
1		islvec.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		fveq2	⊢ ( 𝑓 = 𝑊 → ( Scalar ‘ 𝑓 ) = ( Scalar ‘ 𝑊 ) )
3	2 1	eqtr4di	⊢ ( 𝑓 = 𝑊 → ( Scalar ‘ 𝑓 ) = 𝐹 )
4	3	eleq1d	⊢ ( 𝑓 = 𝑊 → ( ( Scalar ‘ 𝑓 ) ∈ DivRing ↔ 𝐹 ∈ DivRing ) )
5		df-lvec	⊢ LVec = { 𝑓 ∈ LMod ∣ ( Scalar ‘ 𝑓 ) ∈ DivRing }
6	4 5	elrab2	⊢ ( 𝑊 ∈ LVec ↔ ( 𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing ) )