Metamath Proof Explorer

Theorem cnbn

Description: The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007) (New usage is discouraged.)

Ref Expression
Hypothesis cnbn.6 
|- U = <. <. + , x. >. , abs >.
Assertion cnbn 
|- U e. CBan

Proof

Step Hyp Ref Expression
1 cnbn.6 
 |-  U = <. <. + , x. >. , abs >.
2 1 cnnv 
 |-  U e. NrmCVec
3 eqid 
 |-  <. <. + , x. >. , abs >. = <. <. + , x. >. , abs >.
4 eqid 
 |-  ( abs o. - ) = ( abs o. - )
5 3 4 cnims 
 |-  ( abs o. - ) = ( IndMet ` <. <. + , x. >. , abs >. )
6 5 eqcomi 
 |-  ( IndMet ` <. <. + , x. >. , abs >. ) = ( abs o. - )
7 6 cncmet 
 |-  ( IndMet ` <. <. + , x. >. , abs >. ) e. ( CMet ` CC )
8 1 cnnvba 
 |-  CC = ( BaseSet ` U )
9 1 fveq2i 
 |-  ( IndMet ` U ) = ( IndMet ` <. <. + , x. >. , abs >. )
10 9 eqcomi 
 |-  ( IndMet ` <. <. + , x. >. , abs >. ) = ( IndMet ` U )
11 8 10 iscbn 
 |-  ( U e. CBan <-> ( U e. NrmCVec /\ ( IndMet ` <. <. + , x. >. , abs >. ) e. ( CMet ` CC ) ) )
12 2 7 11 mpbir2an 
 |-  U e. CBan