Theorem h2hmetdval

Description: Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h2h.1	|- U = <. <. +h , .h >. , normh >.
	h2h.2	|- U e. NrmCVec
	h2hm.4	|- ~H = ( BaseSet ` U )
	h2hm.5	|- D = ( IndMet ` U )
Assertion	h2hmetdval	|- ( ( A e. ~H /\ B e. ~H ) -> ( A D B ) = ( normh ` ( A -h B ) ) )

Proof

Step	Hyp	Ref	Expression
1		h2h.1	|- U = <. <. +h , .h >. , normh >.
2		h2h.2	|- U e. NrmCVec
3		h2hm.4	|- ~H = ( BaseSet ` U )
4		h2hm.5	|- D = ( IndMet ` U )
5	1 2 3	h2hvs	|- -h = ( -v ` U )
6	1 2	h2hnm	|- normh = ( normCV ` U )
7	3 5 6 4	imsdval	|- ( ( U e. NrmCVec /\ A e. ~H /\ B e. ~H ) -> ( A D B ) = ( normh ` ( A -h B ) ) )
8	2 7	mp3an1	|- ( ( A e. ~H /\ B e. ~H ) -> ( A D B ) = ( normh ` ( A -h B ) ) )