This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in (NrmVec \cap CMetSp) \| Scalar (w) \in CMetSp\}$

Detailed syntax breakdown

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