This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( normh o. -h )
Assertion hilxmet 
|- D e. ( *Met ` ~H )

Proof

Step Hyp Ref Expression
1 hilmet.1 
 |-  D = ( normh o. -h )
2 1 hilmet 
 |-  D e. ( Met ` ~H )
3 metxmet 
 |-  ( D e. ( Met ` ~H ) -> D e. ( *Met ` ~H ) )
4 2 3 ax-mp 
 |-  D e. ( *Met ` ~H )