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 
|- .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. ) )