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

Metamath Proof Explorer

Theorem lssel

Description: A subspace member is a vector. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses lssss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lssss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lssel ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 lssss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lssss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 1 2 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
4 3 sselda ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )