Metamath Proof Explorer

Theorem cnchl

Description: The set of complex numbers is a complex Hilbert space. (Contributed by Steve Rodriguez, 28-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis cnhl.6 
|- U = <. <. + , x. >. , abs >.
Assertion cnchl 
|- U e. CHilOLD

Proof

Step Hyp Ref Expression
1 cnhl.6 
 |-  U = <. <. + , x. >. , abs >.
2 1 cnbn 
 |-  U e. CBan
3 1 cncph 
 |-  U e. CPreHilOLD
4 ishlo 
 |-  ( U e. CHilOLD <-> ( U e. CBan /\ U e. CPreHilOLD ) )
5 2 3 4 mpbir2an 
 |-  U e. CHilOLD