Metamath Proof Explorer


Definition df-hlo

Description: Define the class of all complex Hilbert spaces. A Hilbert space is a Banach space which is also an inner product space. (Contributed by Steve Rodriguez, 28-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion df-hlo
|- CHilOLD = ( CBan i^i CPreHilOLD )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlo
 |-  CHilOLD
1 ccbn
 |-  CBan
2 ccphlo
 |-  CPreHilOLD
3 1 2 cin
 |-  ( CBan i^i CPreHilOLD )
4 0 3 wceq
 |-  CHilOLD = ( CBan i^i CPreHilOLD )