Theorem hlcmet

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

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

Proof

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