Theorem lssn0

Description: A subspace is not empty. (Contributed by NM, 12-Jan-2014) (Revised by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Hypothesis	lssn0.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lssn0	$$⊢U\in S\to U\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		lssn0.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
3		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
4		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
5		eqid	$$⊢{+}_W={+}_W$$
6		eqid	$$⊢{\cdot }_W={\cdot }_W$$
7	2 3 4 5 6 1	islss	$$⊢U\in S\leftrightarrow \left(U\subseteq {\mathrm{Base}}_W\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	simp2bi	$$⊢U\in S\to U\ne \varnothing$$