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 ‘ ℋ )