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	⊢ ( ∃ 𝑥 ∈ ℋ 𝑥 ≠ 0ℎ ↔ ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		helsh	⊢ ℋ ∈ Sℋ
2	1	norm1exi	⊢ ( ∃ 𝑥 ∈ ℋ 𝑥 ≠ 0ℎ ↔ ∃ 𝑦 ∈ ℋ ( normℎ ‘ 𝑦 ) = 1 )