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	⊢ 𝑊 = ( 1st ‘ 𝑈 )
Assertion	hlvc	⊢ ( 𝑈 ∈ CHilOLD → 𝑊 ∈ CVecOLD )

Proof

Step	Hyp	Ref	Expression
1		hlvc.1	⊢ 𝑊 = ( 1st ‘ 𝑈 )
2		hlnv	⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec )
3	1	nvvc	⊢ ( 𝑈 ∈ NrmCVec → 𝑊 ∈ CVecOLD )
4	2 3	syl	⊢ ( 𝑈 ∈ CHilOLD → 𝑊 ∈ CVecOLD )