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

Metamath Proof Explorer

Theorem shne0i

Description: A nonzero subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis shne0.1 
|- A e. SH
Assertion shne0i 
|- ( A =/= 0H <-> E. x e. A x =/= 0h )

Proof

Step Hyp Ref Expression
1 shne0.1 
 |-  A e. SH
2 df-ne 
 |-  ( A =/= 0H <-> -. A = 0H )
3 df-rex 
 |-  ( E. x e. A -. x e. 0H <-> E. x ( x e. A /\ -. x e. 0H ) )
4 nss 
 |-  ( -. A C_ 0H <-> E. x ( x e. A /\ -. x e. 0H ) )
5 shle0 
 |-  ( A e. SH -> ( A C_ 0H <-> A = 0H ) )
6 1 5 ax-mp 
 |-  ( A C_ 0H <-> A = 0H )
7 6 notbii 
 |-  ( -. A C_ 0H <-> -. A = 0H )
8 3 4 7 3bitr2ri 
 |-  ( -. A = 0H <-> E. x e. A -. x e. 0H )
9 elch0 
 |-  ( x e. 0H <-> x = 0h )
10 9 necon3bbii 
 |-  ( -. x e. 0H <-> x =/= 0h )
11 10 rexbii 
 |-  ( E. x e. A -. x e. 0H <-> E. x e. A x =/= 0h )
12 2 8 11 3bitri 
 |-  ( A =/= 0H <-> E. x e. A x =/= 0h )