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	⊢ ( ℋ ≠ 0ℋ ↔ ∃ 𝑥 ∈ ℋ 𝑥 ≠ 0ℎ )

Proof

Step	Hyp	Ref	Expression
1		helch	⊢ ℋ ∈ Cℋ
2	1	chne0i	⊢ ( ℋ ≠ 0ℋ ↔ ∃ 𝑥 ∈ ℋ 𝑥 ≠ 0ℎ )