This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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{˙}{0} = 0_{W}$
		lss0cl.s	$⊢ S = LSubSp (W)$
	Assertion	lssne0	$⊢ X \in S \to (X \neq \{\underset{˙}{0}\} \leftrightarrow \exists y \in X y \neq \underset{˙}{0})$

Proof

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