Theorem lsslvec

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

	Ref	Expression
Hypotheses	lsslvec.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
	lsslvec.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lsslvec	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		lsslvec.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2		lsslvec.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
4	1 2	lsslmod	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LMod )
5	3 4	sylan	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LMod )
6		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7	1 6	resssca	⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
8	7	adantl	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
9	6	lvecdrng	⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
10	9	adantr	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) ∈ DivRing )
11	8 10	eqeltrrd	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑋 ) ∈ DivRing )
12		eqid	⊢ ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑋 )
13	12	islvec	⊢ ( 𝑋 ∈ LVec ↔ ( 𝑋 ∈ LMod ∧ ( Scalar ‘ 𝑋 ) ∈ DivRing ) )
14	5 11 13	sylanbrc	⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LVec )