Metamath Proof Explorer


Theorem hhhl

Description: The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhhl.1 U = + norm
Assertion hhhl U CHil OLD

Proof

Step Hyp Ref Expression
1 hhhl.1 U = + norm
2 1 hhnv U NrmCVec
3 eqid IndMet U = IndMet U
4 1 3 hhcms IndMet U CMet
5 1 hhba = BaseSet U
6 5 3 iscbn U CBan U NrmCVec IndMet U CMet
7 2 4 6 mpbir2an U CBan
8 1 hhph U CPreHil OLD
9 ishlo U CHil OLD U CBan U CPreHil OLD
10 7 8 9 mpbir2an U CHil OLD