Theorem hhxmet

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

	Ref	Expression
Hypotheses	hhnv.1	|- U = <. <. +h , .h >. , normh >.
	hhims2.2	|- D = ( IndMet ` U )
Assertion	hhxmet	|- D e. ( *Met ` ~H )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	|- U = <. <. +h , .h >. , normh >.
2		hhims2.2	|- D = ( IndMet ` U )
3	1 2	hhmet	|- D e. ( Met ` ~H )
4		metxmet	|- ( D e. ( Met ` ~H ) -> D e. ( *Met ` ~H ) )
5	3 4	ax-mp	|- D e. ( *Met ` ~H )