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	syl6eqr	|- ( u = U -> ( IndMet ` u ) = D )
5		fveq2	|- ( u = U -> ( BaseSet ` u ) = ( BaseSet ` U ) )
6	5 1	syl6eqr	|- ( 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 ) ) )