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 30470
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 30466 . 2 class normOpOLD
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 30309 . . 3 class NrmCVec
5 vt . . . 4 setvar 𝑡
63cv 1532 . . . . . 6 class 𝑤
7 cba 30311 . . . . . 6 class BaseSet
86, 7cfv 6534 . . . . 5 class (BaseSet‘𝑤)
92cv 1532 . . . . . 6 class 𝑢
109, 7cfv 6534 . . . . 5 class (BaseSet‘𝑢)
11 cmap 8817 . . . . 5 class m
128, 10, 11co 7402 . . . 4 class ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢))
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1532 . . . . . . . . . 10 class 𝑧
15 cnmcv 30315 . . . . . . . . . . 11 class normCV
169, 15cfv 6534 . . . . . . . . . 10 class (normCV𝑢)
1714, 16cfv 6534 . . . . . . . . 9 class ((normCV𝑢)‘𝑧)
18 c1 11108 . . . . . . . . 9 class 1
19 cle 11247 . . . . . . . . 9 class
2017, 18, 19wbr 5139 . . . . . . . 8 wff ((normCV𝑢)‘𝑧) ≤ 1
21 vx . . . . . . . . . 10 setvar 𝑥
2221cv 1532 . . . . . . . . 9 class 𝑥
235cv 1532 . . . . . . . . . . 11 class 𝑡
2414, 23cfv 6534 . . . . . . . . . 10 class (𝑡𝑧)
256, 15cfv 6534 . . . . . . . . . 10 class (normCV𝑤)
2624, 25cfv 6534 . . . . . . . . 9 class ((normCV𝑤)‘(𝑡𝑧))
2722, 26wceq 1533 . . . . . . . 8 wff 𝑥 = ((normCV𝑤)‘(𝑡𝑧))
2820, 27wa 395 . . . . . . 7 wff (((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
2928, 13, 10wrex 3062 . . . . . 6 wff 𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
3029, 21cab 2701 . . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}
31 cxr 11245 . . . . 5 class *
32 clt 11246 . . . . 5 class <
3330, 31, 32csup 9432 . . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )
345, 12, 33cmpt 5222 . . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < ))
352, 3, 4, 4, 34cmpo 7404 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
361, 35wceq 1533 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  30487
  Copyright terms: Public domain W3C validator