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	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$
Assertion	hilcms	$$⊢D\in \mathrm{CMet}\left(\mathscr{H}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hilcms.1	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$
2		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
3	2 1	hhims	$$⊢D=\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
4	2 3	hhcms	$$⊢D\in \mathrm{CMet}\left(\mathscr{H}\right)$$