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

Metamath Proof Explorer

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 )