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

Definition df-0o 27911
Description: Define the zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-0o 0op = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec𝑤)}))
Distinct variable group:   𝑤,𝑢

Detailed syntax breakdown of Definition df-0o
StepHypRef Expression
1 c0o 27907 . 2 class 0op
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 27748 . . 3 class NrmCVec
52cv 1631 . . . . 5 class 𝑢
6 cba 27750 . . . . 5 class BaseSet
75, 6cfv 6049 . . . 4 class (BaseSet‘𝑢)
83cv 1631 . . . . . 6 class 𝑤
9 cn0v 27752 . . . . . 6 class 0vec
108, 9cfv 6049 . . . . 5 class (0vec𝑤)
1110csn 4321 . . . 4 class {(0vec𝑤)}
127, 11cxp 5264 . . 3 class ((BaseSet‘𝑢) × {(0vec𝑤)})
132, 3, 4, 4, 12cmpt2 6815 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec𝑤)}))
141, 13wceq 1632 1 wff 0op = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec𝑤)}))
Colors of variables: wff setvar class
This definition is referenced by:  0ofval  27951
  Copyright terms: Public domain W3C validator