This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in LVec \leftrightarrow (W \in LMod \land F \in DivRing)$

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