MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-bn Structured version   Visualization version   GIF version

Definition df-bn 22858
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.)
Assertion
Ref Expression
df-bn Ban = {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}

Detailed syntax breakdown of Definition df-bn
StepHypRef Expression
1 cbn 22855 . 2 class Ban
2 vw . . . . . 6 setvar 𝑤
32cv 1473 . . . . 5 class 𝑤
4 csca 15717 . . . . 5 class Scalar
53, 4cfv 5790 . . . 4 class (Scalar‘𝑤)
6 ccms 22854 . . . 4 class CMetSp
75, 6wcel 1976 . . 3 wff (Scalar‘𝑤) ∈ CMetSp
8 cnvc 22137 . . . 4 class NrmVec
98, 6cin 3538 . . 3 class (NrmVec ∩ CMetSp)
107, 2, 9crab 2899 . 2 class {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}
111, 10wceq 1474 1 wff Ban = {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}
Colors of variables: wff setvar class
This definition is referenced by:  isbn  22860
  Copyright terms: Public domain W3C validator