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	|- ( E. x e. ~H x =/= 0h <-> E. y e. ~H ( normh ` y ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		helsh	|- ~H e. SH
2	1	norm1exi	|- ( E. x e. ~H x =/= 0h <-> E. y e. ~H ( normh ` y ) = 1 )