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 V = Base W
lssss.s S = LSubSp W
Assertion lssel U S X U X V

Proof

Step Hyp Ref Expression
1 lssss.v V = Base W
2 lssss.s S = LSubSp W
3 1 2 lssss U S U V
4 3 sselda U S X U X V