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

Definition df-nmoo 28449
Description: Define the norm of an operator between two normed complex vector spaces. This definition produces an operator norm function for each pair of vector spaces 𝑢, 𝑤. Based on definition of linear operator norm in [AkhiezerGlazman] p. 39, although we define it for all operators for convenience. It isn't necessarily meaningful for nonlinear operators, since it doesn't take into account operator values at vectors with norm greater than 1. See Equation 2 of [Kreyszig] p. 92 for a definition that does (although it ignores the value at the zero vector). However, operator norms are rarely if ever used for nonlinear operators. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-nmoo normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
Distinct variable group:   𝑢,𝑡,𝑤,𝑥,𝑧

Detailed syntax breakdown of Definition df-nmoo
StepHypRef Expression
1 cnmoo 28445 . 2 class normOpOLD
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 28288 . . 3 class NrmCVec
5 vt . . . 4 setvar 𝑡
63cv 1527 . . . . . 6 class 𝑤
7 cba 28290 . . . . . 6 class BaseSet
86, 7cfv 6348 . . . . 5 class (BaseSet‘𝑤)
92cv 1527 . . . . . 6 class 𝑢
109, 7cfv 6348 . . . . 5 class (BaseSet‘𝑢)
11 cmap 8395 . . . . 5 class m
128, 10, 11co 7145 . . . 4 class ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢))
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1527 . . . . . . . . . 10 class 𝑧
15 cnmcv 28294 . . . . . . . . . . 11 class normCV
169, 15cfv 6348 . . . . . . . . . 10 class (normCV𝑢)
1714, 16cfv 6348 . . . . . . . . 9 class ((normCV𝑢)‘𝑧)
18 c1 10526 . . . . . . . . 9 class 1
19 cle 10664 . . . . . . . . 9 class
2017, 18, 19wbr 5057 . . . . . . . 8 wff ((normCV𝑢)‘𝑧) ≤ 1
21 vx . . . . . . . . . 10 setvar 𝑥
2221cv 1527 . . . . . . . . 9 class 𝑥
235cv 1527 . . . . . . . . . . 11 class 𝑡
2414, 23cfv 6348 . . . . . . . . . 10 class (𝑡𝑧)
256, 15cfv 6348 . . . . . . . . . 10 class (normCV𝑤)
2624, 25cfv 6348 . . . . . . . . 9 class ((normCV𝑤)‘(𝑡𝑧))
2722, 26wceq 1528 . . . . . . . 8 wff 𝑥 = ((normCV𝑤)‘(𝑡𝑧))
2820, 27wa 396 . . . . . . 7 wff (((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
2928, 13, 10wrex 3136 . . . . . 6 wff 𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
3029, 21cab 2796 . . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}
31 cxr 10662 . . . . 5 class *
32 clt 10663 . . . . 5 class <
3330, 31, 32csup 8892 . . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )
345, 12, 33cmpt 5137 . . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < ))
352, 3, 4, 4, 34cmpo 7147 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
361, 35wceq 1528 1 wff normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoofval  28466
  Copyright terms: Public domain W3C validator