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

Metamath Proof Explorer

Theorem hhmet

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

Ref Expression
Hypotheses hhnv.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
hhims2.2 ⊢ D = IndMet ⁡ U
Assertion hhmet ⊢ D ∈ Met ⁡ ℋ

Proof

Step Hyp Ref Expression
1 hhnv.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 hhims2.2 ⊢ D = IndMet ⁡ U
3 1 hhnv ⊢ U ∈ NrmCVec
4 1 hhba ⊢ ℋ = BaseSet ⁡ U
5 4 2 imsmet ⊢ U ∈ NrmCVec → D ∈ Met ⁡ ℋ
6 3 5 ax-mp ⊢ D ∈ Met ⁡ ℋ