# Metamath Proof Explorer

## Theorem lssss

Description: A subspace is a set of vectors. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses lssss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lssss.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion lssss ${⊢}{U}\in {S}\to {U}\subseteq {V}$

### Proof

Step Hyp Ref Expression
1 lssss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lssss.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
3 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
4 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
5 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
6 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
7 3 4 1 5 6 2 islss ${⊢}{U}\in {S}↔\left({U}\subseteq {V}\wedge {U}\ne \varnothing \wedge \forall {x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {a}\in {U}\phantom{\rule{.4em}{0ex}}\forall {b}\in {U}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{W}}{a}\right){+}_{{W}}{b}\in {U}\right)$
8 7 simp1bi ${⊢}{U}\in {S}\to {U}\subseteq {V}$