This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℎ ∘ - ℎ