Metamath Proof Explorer


Theorem hhmetdval

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

Ref Expression
Hypotheses hhnv.1 U=+norm
hhims2.2 D=IndMetU
Assertion hhmetdval ABADB=normA-B

Proof

Step Hyp Ref Expression
1 hhnv.1 U=+norm
2 hhims2.2 D=IndMetU
3 1 hhnv UNrmCVec
4 1 hhba =BaseSetU
5 1 3 4 2 h2hmetdval ABADB=normA-B