This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )