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={norm}_{ℎ}\circ {-}_{ℎ}$$
Assertion	hilmetdval	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to ADB={norm}_{ℎ}\left(A{-}_{ℎ}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		hilmet.1	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$
2		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
3	2 1	hhims	$$⊢D=\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
4	2 3	hhmetdval	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to ADB={norm}_{ℎ}\left(A{-}_{ℎ}B\right)$$