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