Metamath Proof Explorer


Theorem hilcms

Description: The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hilcms.1 𝐷 = ( norm ∘ − )
Assertion hilcms 𝐷 ∈ ( CMet ‘ ℋ )

Proof

Step Hyp Ref Expression
1 hilcms.1 𝐷 = ( norm ∘ − )
2 eqid ⟨ ⟨ + , · ⟩ , norm ⟩ = ⟨ ⟨ + , · ⟩ , norm
3 2 1 hhims 𝐷 = ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
4 2 3 hhcms 𝐷 ∈ ( CMet ‘ ℋ )