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

Metamath Proof Explorer

Theorem isbn

Description: A Banach space is a normed vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis isbn.1 
|- F = ( Scalar ` W )
Assertion isbn 
|- ( W e. Ban <-> ( W e. NrmVec /\ W e. CMetSp /\ F e. CMetSp ) )

Proof

Step Hyp Ref Expression
1 isbn.1 
 |-  F = ( Scalar ` W )
2 elin 
 |-  ( W e. ( NrmVec i^i CMetSp ) <-> ( W e. NrmVec /\ W e. CMetSp ) )
3 2 anbi1i 
 |-  ( ( W e. ( NrmVec i^i CMetSp ) /\ F e. CMetSp ) <-> ( ( W e. NrmVec /\ W e. CMetSp ) /\ F e. CMetSp ) )
4 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
5 4 1 eqtr4di 
 |-  ( w = W -> ( Scalar ` w ) = F )
6 5 eleq1d 
 |-  ( w = W -> ( ( Scalar ` w ) e. CMetSp <-> F e. CMetSp ) )
7 df-bn 
 |-  Ban = { w e. ( NrmVec i^i CMetSp ) | ( Scalar ` w ) e. CMetSp }
8 6 7 elrab2 
 |-  ( W e. Ban <-> ( W e. ( NrmVec i^i CMetSp ) /\ F e. CMetSp ) )
9 df-3an 
 |-  ( ( W e. NrmVec /\ W e. CMetSp /\ F e. CMetSp ) <-> ( ( W e. NrmVec /\ W e. CMetSp ) /\ F e. CMetSp ) )
10 3 8 9 3bitr4i 
 |-  ( W e. Ban <-> ( W e. NrmVec /\ W e. CMetSp /\ F e. CMetSp ) )