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	$$⊢\mathscr{H}\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in \mathscr{H}x\ne 0_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	chne0i	$$⊢\mathscr{H}\ne 0_{\mathscr{H}}\leftrightarrow \exists x\in \mathscr{H}x\ne 0_{ℎ}$$