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 = { 𝑤 ∈ ( 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 }