Metamath Proof Explorer


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 )