Theorem hilmetdval

Description: Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 17-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hilmet.1	|- D = ( normh o. -h )
Assertion	hilmetdval	|- ( ( A e. ~H /\ B e. ~H ) -> ( A D B ) = ( normh ` ( A -h B ) ) )

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	hhmetdval	|- ( ( A e. ~H /\ B e. ~H ) -> ( A D B ) = ( normh ` ( A -h B ) ) )