Metamath Proof Explorer

Theorem chne0i

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

Ref Expression
Hypothesis ch0le.1 
|- A e. CH
Assertion chne0i 
|- ( A =/= 0H <-> E. x e. A x =/= 0h )

Proof

Step Hyp Ref Expression
1 ch0le.1 
 |-  A e. CH
2 1 chshii 
 |-  A e. SH
3 2 shne0i 
 |-  ( A =/= 0H <-> E. x e. A x =/= 0h )