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\leftrightarrow \left(U\subseteq V\wedge U\ne \varnothing \wedge \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall a\in U\forall b\in U\left(x{\cdot }_{W}a\right){+}_{W}b\in U\right)$$
8	7	simp1bi	$$⊢U\in S\to U\subseteq V$$