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 30266
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 30262 . 2 class normOpOLD
2 vu . . 3 setvar 𝑒
3 vw . . 3 setvar 𝑀
4 cnv 30105 . . 3 class NrmCVec
5 vt . . . 4 setvar 𝑑
63cv 1539 . . . . . 6 class 𝑀
7 cba 30107 . . . . . 6 class BaseSet
86, 7cfv 6543 . . . . 5 class (BaseSetβ€˜π‘€)
92cv 1539 . . . . . 6 class 𝑒
109, 7cfv 6543 . . . . 5 class (BaseSetβ€˜π‘’)
11 cmap 8823 . . . . 5 class ↑m
128, 10, 11co 7412 . . . 4 class ((BaseSetβ€˜π‘€) ↑m (BaseSetβ€˜π‘’))
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1539 . . . . . . . . . 10 class 𝑧
15 cnmcv 30111 . . . . . . . . . . 11 class normCV
169, 15cfv 6543 . . . . . . . . . 10 class (normCVβ€˜π‘’)
1714, 16cfv 6543 . . . . . . . . 9 class ((normCVβ€˜π‘’)β€˜π‘§)
18 c1 11114 . . . . . . . . 9 class 1
19 cle 11254 . . . . . . . . 9 class ≀
2017, 18, 19wbr 5148 . . . . . . . 8 wff ((normCVβ€˜π‘’)β€˜π‘§) ≀ 1
21 vx . . . . . . . . . 10 setvar π‘₯
2221cv 1539 . . . . . . . . 9 class π‘₯
235cv 1539 . . . . . . . . . . 11 class 𝑑
2414, 23cfv 6543 . . . . . . . . . 10 class (π‘‘β€˜π‘§)
256, 15cfv 6543 . . . . . . . . . 10 class (normCVβ€˜π‘€)
2624, 25cfv 6543 . . . . . . . . 9 class ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§))
2722, 26wceq 1540 . . . . . . . 8 wff π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§))
2820, 27wa 395 . . . . . . 7 wff (((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))
2928, 13, 10wrex 3069 . . . . . 6 wff βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))
3029, 21cab 2708 . . . . 5 class {π‘₯ ∣ βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))}
31 cxr 11252 . . . . 5 class ℝ*
32 clt 11253 . . . . 5 class <
3330, 31, 32csup 9438 . . . 4 class sup({π‘₯ ∣ βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))}, ℝ*, < )
345, 12, 33cmpt 5231 . . 3 class (𝑑 ∈ ((BaseSetβ€˜π‘€) ↑m (BaseSetβ€˜π‘’)) ↦ sup({π‘₯ ∣ βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))}, ℝ*, < ))
352, 3, 4, 4, 34cmpo 7414 . 2 class (𝑒 ∈ NrmCVec, 𝑀 ∈ NrmCVec ↦ (𝑑 ∈ ((BaseSetβ€˜π‘€) ↑m (BaseSetβ€˜π‘’)) ↦ sup({π‘₯ ∣ βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))}, ℝ*, < )))
361, 35wceq 1540 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  30283
  Copyright terms: Public domain W3C validator