Metamath Proof Explorer


Theorem hhmet

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 )

Proof

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 )