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 28151
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‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
Distinct variable group:   𝑢,𝑡,𝑤,𝑥,𝑧

Detailed syntax breakdown of Definition df-nmoo
StepHypRef Expression
1 cnmoo 28147 . 2 class normOpOLD
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 27990 . . 3 class NrmCVec
5 vt . . . 4 setvar 𝑡
63cv 1655 . . . . . 6 class 𝑤
7 cba 27992 . . . . . 6 class BaseSet
86, 7cfv 6127 . . . . 5 class (BaseSet‘𝑤)
92cv 1655 . . . . . 6 class 𝑢
109, 7cfv 6127 . . . . 5 class (BaseSet‘𝑢)
11 cmap 8127 . . . . 5 class 𝑚
128, 10, 11co 6910 . . . 4 class ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢))
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1655 . . . . . . . . . 10 class 𝑧
15 cnmcv 27996 . . . . . . . . . . 11 class normCV
169, 15cfv 6127 . . . . . . . . . 10 class (normCV𝑢)
1714, 16cfv 6127 . . . . . . . . 9 class ((normCV𝑢)‘𝑧)
18 c1 10260 . . . . . . . . 9 class 1
19 cle 10399 . . . . . . . . 9 class
2017, 18, 19wbr 4875 . . . . . . . 8 wff ((normCV𝑢)‘𝑧) ≤ 1
21 vx . . . . . . . . . 10 setvar 𝑥
2221cv 1655 . . . . . . . . 9 class 𝑥
235cv 1655 . . . . . . . . . . 11 class 𝑡
2414, 23cfv 6127 . . . . . . . . . 10 class (𝑡𝑧)
256, 15cfv 6127 . . . . . . . . . 10 class (normCV𝑤)
2624, 25cfv 6127 . . . . . . . . 9 class ((normCV𝑤)‘(𝑡𝑧))
2722, 26wceq 1656 . . . . . . . 8 wff 𝑥 = ((normCV𝑤)‘(𝑡𝑧))
2820, 27wa 386 . . . . . . 7 wff (((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
2928, 13, 10wrex 3118 . . . . . 6 wff 𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
3029, 21cab 2811 . . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}
31 cxr 10397 . . . . 5 class *
32 clt 10398 . . . . 5 class <
3330, 31, 32csup 8621 . . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )
345, 12, 33cmpt 4954 . . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < ))
352, 3, 4, 4, 34cmpt2 6912 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
361, 35wceq 1656 1 wff normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoofval  28168
  Copyright terms: Public domain W3C validator