Theorem hilcms

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

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

Proof

Step	Hyp	Ref	Expression
1		hilcms.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	hhcms	|- D e. ( CMet ` ~H )