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

Definition df-bn 23943
 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 23940 . 2 class Ban
2 vw . . . . . 6 setvar 𝑤
32cv 1537 . . . . 5 class 𝑤
4 csca 16568 . . . . 5 class Scalar
53, 4cfv 6343 . . . 4 class (Scalar‘𝑤)
6 ccms 23939 . . . 4 class CMetSp
75, 6wcel 2115 . . 3 wff (Scalar‘𝑤) ∈ CMetSp
8 cnvc 23191 . . . 4 class NrmVec
98, 6cin 3918 . . 3 class (NrmVec ∩ CMetSp)
107, 2, 9crab 3137 . 2 class {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}
111, 10wceq 1538 1 wff Ban = {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}
 Colors of variables: wff setvar class This definition is referenced by:  isbn  23945
 Copyright terms: Public domain W3C validator