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 ) |
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 ) |