Description: The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hhnv.1 | |- U = <. <. +h , .h >. , normh >. |
|
hhims2.2 | |- D = ( IndMet ` U ) |
||
Assertion | hhmet | |- D e. ( Met ` ~H ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hhnv.1 | |- U = <. <. +h , .h >. , normh >. |
|
2 | hhims2.2 | |- D = ( IndMet ` U ) |
|
3 | 1 | hhnv | |- U e. NrmCVec |
4 | 1 | hhba | |- ~H = ( BaseSet ` U ) |
5 | 4 2 | imsmet | |- ( U e. NrmCVec -> D e. ( Met ` ~H ) ) |
6 | 3 5 | ax-mp | |- D e. ( Met ` ~H ) |