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	$$⊢\mathrm{Ban}=\left\{w\in \left(\mathrm{NrmVec}\cap \mathrm{CMetSp}\right)|\mathrm{Scalar}\left(w\right)\in \mathrm{CMetSp}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbn	$$class\mathrm{Ban}$$
1		vw	$$setvarw$$
2		cnvc	$$class\mathrm{NrmVec}$$
3		ccms	$$class\mathrm{CMetSp}$$
4	2 3	cin	$$class\left(\mathrm{NrmVec}\cap \mathrm{CMetSp}\right)$$
5		csca	$$class\mathrm{Scalar}$$
6	1	cv	$$setvarw$$
7	6 5	cfv	$$class\mathrm{Scalar}\left(w\right)$$
8	7 3	wcel	$$wff\mathrm{Scalar}\left(w\right)\in \mathrm{CMetSp}$$
9	8 1 4	crab	$$class\left\{w\in \left(\mathrm{NrmVec}\cap \mathrm{CMetSp}\right)|\mathrm{Scalar}\left(w\right)\in \mathrm{CMetSp}\right\}$$
10	0 9	wceq	$$wff\mathrm{Ban}=\left\{w\in \left(\mathrm{NrmVec}\cap \mathrm{CMetSp}\right)|\mathrm{Scalar}\left(w\right)\in \mathrm{CMetSp}\right\}$$