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

Metamath Proof Explorer

Theorem lbsel

Description: An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lbsss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lbsss.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
Assertion lbsel ( ( 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝐸 ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 lbsss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lbsss.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3 1 2 lbsss ⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉 )
4 3 sselda ⊢ ( ( 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝐸 ∈ 𝑉 )