Metamath Proof Explorer

Theorem lsslvec

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

Ref Expression
Hypotheses lsslvec.x ⊢ X = W ↾ 𝑠 U
lsslvec.s ⊢ S = LSubSp ⁡ W
Assertion lsslvec ⊢ W ∈ LVec ∧ U ∈ S → X ∈ LVec

Proof

Step Hyp Ref Expression
1 lsslvec.x ⊢ X = W ↾ 𝑠 U
2 lsslvec.s ⊢ S = LSubSp ⁡ W
3 lveclmod ⊢ W ∈ LVec → W ∈ LMod
4 1 2 lsslmod ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LMod
5 3 4 sylan ⊢ W ∈ LVec ∧ U ∈ S → X ∈ LMod
6 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
7 1 6 resssca ⊢ U ∈ S → Scalar ⁡ W = Scalar ⁡ X
8 7 adantl ⊢ W ∈ LVec ∧ U ∈ S → Scalar ⁡ W = Scalar ⁡ X
9 6 lvecdrng ⊢ W ∈ LVec → Scalar ⁡ W ∈ DivRing
10 9 adantr ⊢ W ∈ LVec ∧ U ∈ S → Scalar ⁡ W ∈ DivRing
11 8 10 eqeltrrd ⊢ W ∈ LVec ∧ U ∈ S → Scalar ⁡ X ∈ DivRing
12 eqid ⊢ Scalar ⁡ X = Scalar ⁡ X
13 12 islvec ⊢ X ∈ LVec ↔ X ∈ LMod ∧ Scalar ⁡ X ∈ DivRing
14 5 11 13 sylanbrc ⊢ W ∈ LVec ∧ U ∈ S → X ∈ LVec