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 )