Metamath Proof Explorer


Theorem iscbn

Description: A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006) Use isbn instead. (New usage is discouraged.)

Ref Expression
Hypotheses iscbn.x
|- X = ( BaseSet ` U )
iscbn.8
|- D = ( IndMet ` U )
Assertion iscbn
|- ( U e. CBan <-> ( U e. NrmCVec /\ D e. ( CMet ` X ) ) )

Proof

Step Hyp Ref Expression
1 iscbn.x
 |-  X = ( BaseSet ` U )
2 iscbn.8
 |-  D = ( IndMet ` U )
3 fveq2
 |-  ( u = U -> ( IndMet ` u ) = ( IndMet ` U ) )
4 3 2 eqtr4di
 |-  ( u = U -> ( IndMet ` u ) = D )
5 fveq2
 |-  ( u = U -> ( BaseSet ` u ) = ( BaseSet ` U ) )
6 5 1 eqtr4di
 |-  ( u = U -> ( BaseSet ` u ) = X )
7 6 fveq2d
 |-  ( u = U -> ( CMet ` ( BaseSet ` u ) ) = ( CMet ` X ) )
8 4 7 eleq12d
 |-  ( u = U -> ( ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) ) <-> D e. ( CMet ` X ) ) )
9 df-cbn
 |-  CBan = { u e. NrmCVec | ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) ) }
10 8 9 elrab2
 |-  ( U e. CBan <-> ( U e. NrmCVec /\ D e. ( CMet ` X ) ) )