Theorem lssne0

Description: A nonzero subspace has a nonzero vector. ( shne0i analog.) (Contributed by NM, 20-Apr-2014) (Proof shortened by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Hypotheses	lss0cl.z	$$⊢\underset{\dot{}}{0}=0_W$$
	lss0cl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lssne0	$$⊢X\in S\to \left(X\ne \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \exists y\in Xy\ne \underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lss0cl.z	$$⊢\underset{\dot{}}{0}=0_W$$
2		lss0cl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3	2	lssn0	$$⊢X\in S\to X\ne \varnothing$$
4		eqsn	$$⊢X\ne \varnothing \to \left(X=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall y\in Xy=\underset{\dot{}}{0}\right)$$
5	3 4	syl	$$⊢X\in S\to \left(X=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall y\in Xy=\underset{\dot{}}{0}\right)$$
6		nne	$$⊢\neg y\ne \underset{\dot{}}{0}\leftrightarrow y=\underset{\dot{}}{0}$$
7	6	ralbii	$$⊢\forall y\in X\neg y\ne \underset{\dot{}}{0}\leftrightarrow \forall y\in Xy=\underset{\dot{}}{0}$$
8		ralnex	$$⊢\forall y\in X\neg y\ne \underset{\dot{}}{0}\leftrightarrow \neg \exists y\in Xy\ne \underset{\dot{}}{0}$$
9	7 8	bitr3i	$$⊢\forall y\in Xy=\underset{\dot{}}{0}\leftrightarrow \neg \exists y\in Xy\ne \underset{\dot{}}{0}$$
10	5 9	bitr2di	$$⊢X\in S\to \left(\neg \exists y\in Xy\ne \underset{\dot{}}{0}\leftrightarrow X=\left\{\underset{\dot{}}{0}\right\}\right)$$
11	10	necon1abid	$$⊢X\in S\to \left(X\ne \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \exists y\in Xy\ne \underset{\dot{}}{0}\right)$$