Metamath Proof Explorer


Theorem hhims2

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

Ref Expression
Hypotheses hhnv.1 U = + norm
hhims2.2 D = IndMet U
Assertion hhims2 D = norm -

Proof

Step Hyp Ref Expression
1 hhnv.1 U = + norm
2 hhims2.2 D = IndMet U
3 eqid norm - = norm -
4 1 3 hhims norm - = IndMet U
5 2 4 eqtr4i D = norm -