Theorem hlvc

Description: Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hlvc.1	|- W = ( 1st ` U )
Assertion	hlvc	|- ( U e. CHilOLD -> W e. CVecOLD )

Proof

Step	Hyp	Ref	Expression
1		hlvc.1	|- W = ( 1st ` U )
2		hlnv	|- ( U e. CHilOLD -> U e. NrmCVec )
3	1	nvvc	|- ( U e. NrmCVec -> W e. CVecOLD )
4	2 3	syl	|- ( U e. CHilOLD -> W e. CVecOLD )