Theorem hilmet

Description: The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hilmet.1	|- D = ( normh o. -h )
Assertion	hilmet	|- D e. ( Met ` ~H )

Proof

Step	Hyp	Ref	Expression
1		hilmet.1	|- D = ( normh o. -h )
2		eqid	|- <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
3	2 1	hhims	|- D = ( IndMet ` <. <. +h , .h >. , normh >. )
4	2 3	hhmet	|- D e. ( Met ` ~H )