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=1^{st}\left(U\right)$$
Assertion	hlvc	$$⊢U\in {CHil}_{\mathrm{OLD}}\to W\in {CVec}_{\mathrm{OLD}}$$

Proof

Step	Hyp	Ref	Expression
1		hlvc.1	$$⊢W=1^{st}\left(U\right)$$
2		hlnv	$$⊢U\in {CHil}_{\mathrm{OLD}}\to U\in \mathrm{NrmCVec}$$
3	1	nvvc	$$⊢U\in \mathrm{NrmCVec}\to W\in {CVec}_{\mathrm{OLD}}$$
4	2 3	syl	$$⊢U\in {CHil}_{\mathrm{OLD}}\to W\in {CVec}_{\mathrm{OLD}}$$