Theorem norm1hex

Description: A normalized vector can exist only iff the Hilbert space has a nonzero vector. (Contributed by NM, 21-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	norm1hex	$$⊢\exists x\in \mathscr{H}x\ne 0_{ℎ}\leftrightarrow \exists y\in \mathscr{H}{norm}_{ℎ}\left(y\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		helsh	$$⊢\mathscr{H}\in {\mathbf{S}}_{\mathscr{H}}$$
2	1	norm1exi	$$⊢\exists x\in \mathscr{H}x\ne 0_{ℎ}\leftrightarrow \exists y\in \mathscr{H}{norm}_{ℎ}\left(y\right)=1$$