Theorem hilmet

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

	Ref	Expression
Hypothesis	hilmet.1	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$
Assertion	hilmet	$$⊢D\in \mathrm{Met}\left(\mathscr{H}\right)$$

Proof

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