Theorem hilxmet

Description: The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hilmet.1	$$⊢D={norm}_{ℎ}\circ {-}_{ℎ}$$
2	1	hilmet	$$⊢D\in \mathrm{Met}\left(\mathscr{H}\right)$$
3		metxmet	$$⊢D\in \mathrm{Met}\left(\mathscr{H}\right)\to D\in \mathrm{\infty Met}\left(\mathscr{H}\right)$$
4	2 3	ax-mp	$$⊢D\in \mathrm{\infty Met}\left(\mathscr{H}\right)$$