Metamath Proof Explorer


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 LVec W LMod F 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 DivRing F DivRing
5 df-lvec LVec = f LMod | Scalar f DivRing
6 4 5 elrab2 W LVec W LMod F DivRing