Theorem islvec

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

	Ref	Expression
Hypothesis	islvec.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
Assertion	islvec	$$⊢W\in \mathrm{LVec}\leftrightarrow \left(W\in \mathrm{LMod}\wedge F\in \mathrm{DivRing}\right)$$

Proof

Step	Hyp	Ref	Expression
1		islvec.1	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		fveq2	$$⊢f=W\to \mathrm{Scalar}\left(f\right)=\mathrm{Scalar}\left(W\right)$$
3	2 1	eqtr4di	$$⊢f=W\to \mathrm{Scalar}\left(f\right)=F$$
4	3	eleq1d	$$⊢f=W\to \left(\mathrm{Scalar}\left(f\right)\in \mathrm{DivRing}\leftrightarrow F\in \mathrm{DivRing}\right)$$
5		df-lvec	$$⊢\mathrm{LVec}=\left\{f\in \mathrm{LMod}|\mathrm{Scalar}\left(f\right)\in \mathrm{DivRing}\right\}$$
6	4 5	elrab2	$$⊢W\in \mathrm{LVec}\leftrightarrow \left(W\in \mathrm{LMod}\wedge F\in \mathrm{DivRing}\right)$$