Theorem lsslvec

Description: A vector subspace is a vector space. (Contributed by NM, 14-Mar-2015)

	Ref	Expression
Hypotheses	lsslvec.x	|- X = ( W |`s U )
	lsslvec.s	|- S = ( LSubSp ` W )
Assertion	lsslvec	|- ( ( W e. LVec /\ U e. S ) -> X e. LVec )

Proof

Step	Hyp	Ref	Expression
1		lsslvec.x	|- X = ( W |`s U )
2		lsslvec.s	|- S = ( LSubSp ` W )
3		lveclmod	|- ( W e. LVec -> W e. LMod )
4	1 2	lsslmod	|- ( ( W e. LMod /\ U e. S ) -> X e. LMod )
5	3 4	sylan	|- ( ( W e. LVec /\ U e. S ) -> X e. LMod )
6		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
7	1 6	resssca	|- ( U e. S -> ( Scalar ` W ) = ( Scalar ` X ) )
8	7	adantl	|- ( ( W e. LVec /\ U e. S ) -> ( Scalar ` W ) = ( Scalar ` X ) )
9	6	lvecdrng	|- ( W e. LVec -> ( Scalar ` W ) e. DivRing )
10	9	adantr	|- ( ( W e. LVec /\ U e. S ) -> ( Scalar ` W ) e. DivRing )
11	8 10	eqeltrrd	|- ( ( W e. LVec /\ U e. S ) -> ( Scalar ` X ) e. DivRing )
12		eqid	|- ( Scalar ` X ) = ( Scalar ` X )
13	12	islvec	|- ( X e. LVec <-> ( X e. LMod /\ ( Scalar ` X ) e. DivRing ) )
14	5 11 13	sylanbrc	|- ( ( W e. LVec /\ U e. S ) -> X e. LVec )