Theorem hlmet

Description: The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlcmet.x	|- X = ( BaseSet ` U )
	hlcmet.8	|- D = ( IndMet ` U )
Assertion	hlmet	|- ( U e. CHilOLD -> D e. ( Met ` X ) )

Proof

Step	Hyp	Ref	Expression
1		hlcmet.x	|- X = ( BaseSet ` U )
2		hlcmet.8	|- D = ( IndMet ` U )
3	1 2	hlcmet	|- ( U e. CHilOLD -> D e. ( CMet ` X ) )
4		cmetmet	|- ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
5	3 4	syl	|- ( U e. CHilOLD -> D e. ( Met ` X ) )