Definition df-bn

Description: Define the class of all Banach spaces. A Banach space is a normed vector space such that both the vector space and the scalar field are complete under their respective norm-induced metrics. (Contributed by NM, 5-Dec-2006) (Revised by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Assertion	df-bn	|- Ban = { w e. ( NrmVec i^i CMetSp ) | ( Scalar ` w ) e. CMetSp }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbn	|- Ban
1		vw	|- w
2		cnvc	|- NrmVec
3		ccms	|- CMetSp
4	2 3	cin	|- ( NrmVec i^i CMetSp )
5		csca	|- Scalar
6	1	cv	|- w
7	6 5	cfv	|- ( Scalar ` w )
8	7 3	wcel	|- ( Scalar ` w ) e. CMetSp
9	8 1 4	crab	|- { w e. ( NrmVec i^i CMetSp ) | ( Scalar ` w ) e. CMetSp }
10	0 9	wceq	|- Ban = { w e. ( NrmVec i^i CMetSp ) | ( Scalar ` w ) e. CMetSp }