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

Definition df-nmoo 27909
 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 27905 . 2 class normOpOLD
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 27748 . . 3 class NrmCVec
5 vt . . . 4 setvar 𝑡
63cv 1631 . . . . . 6 class 𝑤
7 cba 27750 . . . . . 6 class BaseSet
86, 7cfv 6049 . . . . 5 class (BaseSet‘𝑤)
92cv 1631 . . . . . 6 class 𝑢
109, 7cfv 6049 . . . . 5 class (BaseSet‘𝑢)
11 cmap 8023 . . . . 5 class 𝑚
128, 10, 11co 6813 . . . 4 class ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢))
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1631 . . . . . . . . . 10 class 𝑧
15 cnmcv 27754 . . . . . . . . . . 11 class normCV
169, 15cfv 6049 . . . . . . . . . 10 class (normCV𝑢)
1714, 16cfv 6049 . . . . . . . . 9 class ((normCV𝑢)‘𝑧)
18 c1 10129 . . . . . . . . 9 class 1
19 cle 10267 . . . . . . . . 9 class
2017, 18, 19wbr 4804 . . . . . . . 8 wff ((normCV𝑢)‘𝑧) ≤ 1
21 vx . . . . . . . . . 10 setvar 𝑥
2221cv 1631 . . . . . . . . 9 class 𝑥
235cv 1631 . . . . . . . . . . 11 class 𝑡
2414, 23cfv 6049 . . . . . . . . . 10 class (𝑡𝑧)
256, 15cfv 6049 . . . . . . . . . 10 class (normCV𝑤)
2624, 25cfv 6049 . . . . . . . . 9 class ((normCV𝑤)‘(𝑡𝑧))
2722, 26wceq 1632 . . . . . . . 8 wff 𝑥 = ((normCV𝑤)‘(𝑡𝑧))
2820, 27wa 383 . . . . . . 7 wff (((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
2928, 13, 10wrex 3051 . . . . . 6 wff 𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
3029, 21cab 2746 . . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}
31 cxr 10265 . . . . 5 class *
32 clt 10266 . . . . 5 class <
3330, 31, 32csup 8511 . . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )
345, 12, 33cmpt 4881 . . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < ))
352, 3, 4, 4, 34cmpt2 6815 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
361, 35wceq 1632 1 wff normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
 Colors of variables: wff setvar class This definition is referenced by:  nmoofval  27926
 Copyright terms: Public domain W3C validator