Metamath Proof Explorer

Theorem hne0

Description: Hilbert space has a nonzero vector iff it is not trivial. (Contributed by NM, 24-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion hne0 
|- ( ~H =/= 0H <-> E. x e. ~H x =/= 0h )

Proof

Step Hyp Ref Expression
1 helch 
 |-  ~H e. CH
2 1 chne0i 
 |-  ( ~H =/= 0H <-> E. x e. ~H x =/= 0h )