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 = { 𝑤 ∈ ( NrmVec ∩ CMetSp ) ∣ ( Scalar ‘ 𝑤 ) ∈ CMetSp }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbn	⊢ Ban
1		vw	⊢ 𝑤
2		cnvc	⊢ NrmVec
3		ccms	⊢ CMetSp
4	2 3	cin	⊢ ( NrmVec ∩ CMetSp )
5		csca	⊢ Scalar
6	1	cv	⊢ 𝑤
7	6 5	cfv	⊢ ( Scalar ‘ 𝑤 )
8	7 3	wcel	⊢ ( Scalar ‘ 𝑤 ) ∈ CMetSp
9	8 1 4	crab	⊢ { 𝑤 ∈ ( NrmVec ∩ CMetSp ) ∣ ( Scalar ‘ 𝑤 ) ∈ CMetSp }
10	0 9	wceq	⊢ Ban = { 𝑤 ∈ ( NrmVec ∩ CMetSp ) ∣ ( Scalar ‘ 𝑤 ) ∈ CMetSp }