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 27728
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 27724 . 2 class normOpOLD
2 vu . . 3 setvar 𝑢
3 vw . . 3 setvar 𝑤
4 cnv 27567 . . 3 class NrmCVec
5 vt . . . 4 setvar 𝑡
63cv 1522 . . . . . 6 class 𝑤
7 cba 27569 . . . . . 6 class BaseSet
86, 7cfv 5926 . . . . 5 class (BaseSet‘𝑤)
92cv 1522 . . . . . 6 class 𝑢
109, 7cfv 5926 . . . . 5 class (BaseSet‘𝑢)
11 cmap 7899 . . . . 5 class 𝑚
128, 10, 11co 6690 . . . 4 class ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢))
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1522 . . . . . . . . . 10 class 𝑧
15 cnmcv 27573 . . . . . . . . . . 11 class normCV
169, 15cfv 5926 . . . . . . . . . 10 class (normCV𝑢)
1714, 16cfv 5926 . . . . . . . . 9 class ((normCV𝑢)‘𝑧)
18 c1 9975 . . . . . . . . 9 class 1
19 cle 10113 . . . . . . . . 9 class
2017, 18, 19wbr 4685 . . . . . . . 8 wff ((normCV𝑢)‘𝑧) ≤ 1
21 vx . . . . . . . . . 10 setvar 𝑥
2221cv 1522 . . . . . . . . 9 class 𝑥
235cv 1522 . . . . . . . . . . 11 class 𝑡
2414, 23cfv 5926 . . . . . . . . . 10 class (𝑡𝑧)
256, 15cfv 5926 . . . . . . . . . 10 class (normCV𝑤)
2624, 25cfv 5926 . . . . . . . . 9 class ((normCV𝑤)‘(𝑡𝑧))
2722, 26wceq 1523 . . . . . . . 8 wff 𝑥 = ((normCV𝑤)‘(𝑡𝑧))
2820, 27wa 383 . . . . . . 7 wff (((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
2928, 13, 10wrex 2942 . . . . . 6 wff 𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))
3029, 21cab 2637 . . . . 5 class {𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}
31 cxr 10111 . . . . 5 class *
32 clt 10112 . . . . 5 class <
3330, 31, 32csup 8387 . . . 4 class sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )
345, 12, 33cmpt 4762 . . 3 class (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < ))
352, 3, 4, 4, 34cmpt2 6692 . 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
361, 35wceq 1523 1 wff normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV𝑤)‘(𝑡𝑧)))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoofval  27745
  Copyright terms: Public domain W3C validator