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 ‘ ℋ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hilcms.1 | ⊢ 𝐷 = ( normℎ ∘ −ℎ ) | |
2 | eqid | ⊢ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 = 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 | |
3 | 2 1 | hhims | ⊢ 𝐷 = ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
4 | 2 3 | hhcms | ⊢ 𝐷 ∈ ( CMet ‘ ℋ ) |