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	|- .0. = ( 0g ` W )
	lss0cl.s	|- S = ( LSubSp ` W )
Assertion	lssne0	|- ( X e. S -> ( X =/= { .0. } <-> E. y e. X y =/= .0. ) )

Proof

Step	Hyp	Ref	Expression
1		lss0cl.z	|- .0. = ( 0g ` W )
2		lss0cl.s	|- S = ( LSubSp ` W )
3	2	lssn0	|- ( X e. S -> X =/= (/) )
4		eqsn	|- ( X =/= (/) -> ( X = { .0. } <-> A. y e. X y = .0. ) )
5	3 4	syl	|- ( X e. S -> ( X = { .0. } <-> A. y e. X y = .0. ) )
6		nne	|- ( -. y =/= .0. <-> y = .0. )
7	6	ralbii	|- ( A. y e. X -. y =/= .0. <-> A. y e. X y = .0. )
8		ralnex	|- ( A. y e. X -. y =/= .0. <-> -. E. y e. X y =/= .0. )
9	7 8	bitr3i	|- ( A. y e. X y = .0. <-> -. E. y e. X y =/= .0. )
10	5 9	bitr2di	|- ( X e. S -> ( -. E. y e. X y =/= .0. <-> X = { .0. } ) )
11	10	necon1abid	|- ( X e. S -> ( X =/= { .0. } <-> E. y e. X y =/= .0. ) )