This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )