This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⁡ U
Assertion hlvc ⊢ U ∈ CHil OLD → W ∈ CVec OLD

Proof

Step Hyp Ref Expression
1 hlvc.1 ⊢ W = 1 st ⁡ U
2 hlnv ⊢ U ∈ CHil OLD → U ∈ NrmCVec
3 1 nvvc ⊢ U ∈ NrmCVec → W ∈ CVec OLD
4 2 3 syl ⊢ U ∈ CHil OLD → W ∈ CVec OLD