Metamath Proof Explorer


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-
Assertion hilxmet D∞Met

Proof

Step Hyp Ref Expression
1 hilmet.1 D=norm-
2 1 hilmet DMet
3 metxmet DMetD∞Met
4 2 3 ax-mp D∞Met