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 30029
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 30025 . 2 class normOpOLD
2 vu . . 3 setvar 𝑒
3 vw . . 3 setvar 𝑀
4 cnv 29868 . . 3 class NrmCVec
5 vt . . . 4 setvar 𝑑
63cv 1541 . . . . . 6 class 𝑀
7 cba 29870 . . . . . 6 class BaseSet
86, 7cfv 6544 . . . . 5 class (BaseSetβ€˜π‘€)
92cv 1541 . . . . . 6 class 𝑒
109, 7cfv 6544 . . . . 5 class (BaseSetβ€˜π‘’)
11 cmap 8820 . . . . 5 class ↑m
128, 10, 11co 7409 . . . 4 class ((BaseSetβ€˜π‘€) ↑m (BaseSetβ€˜π‘’))
13 vz . . . . . . . . . . 11 setvar 𝑧
1413cv 1541 . . . . . . . . . 10 class 𝑧
15 cnmcv 29874 . . . . . . . . . . 11 class normCV
169, 15cfv 6544 . . . . . . . . . 10 class (normCVβ€˜π‘’)
1714, 16cfv 6544 . . . . . . . . 9 class ((normCVβ€˜π‘’)β€˜π‘§)
18 c1 11111 . . . . . . . . 9 class 1
19 cle 11249 . . . . . . . . 9 class ≀
2017, 18, 19wbr 5149 . . . . . . . 8 wff ((normCVβ€˜π‘’)β€˜π‘§) ≀ 1
21 vx . . . . . . . . . 10 setvar π‘₯
2221cv 1541 . . . . . . . . 9 class π‘₯
235cv 1541 . . . . . . . . . . 11 class 𝑑
2414, 23cfv 6544 . . . . . . . . . 10 class (π‘‘β€˜π‘§)
256, 15cfv 6544 . . . . . . . . . 10 class (normCVβ€˜π‘€)
2624, 25cfv 6544 . . . . . . . . 9 class ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§))
2722, 26wceq 1542 . . . . . . . 8 wff π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§))
2820, 27wa 397 . . . . . . 7 wff (((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))
2928, 13, 10wrex 3071 . . . . . 6 wff βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))
3029, 21cab 2710 . . . . 5 class {π‘₯ ∣ βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))}
31 cxr 11247 . . . . 5 class ℝ*
32 clt 11248 . . . . 5 class <
3330, 31, 32csup 9435 . . . 4 class sup({π‘₯ ∣ βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))}, ℝ*, < )
345, 12, 33cmpt 5232 . . 3 class (𝑑 ∈ ((BaseSetβ€˜π‘€) ↑m (BaseSetβ€˜π‘’)) ↦ sup({π‘₯ ∣ βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))}, ℝ*, < ))
352, 3, 4, 4, 34cmpo 7411 . 2 class (𝑒 ∈ NrmCVec, 𝑀 ∈ NrmCVec ↦ (𝑑 ∈ ((BaseSetβ€˜π‘€) ↑m (BaseSetβ€˜π‘’)) ↦ sup({π‘₯ ∣ βˆƒπ‘§ ∈ (BaseSetβ€˜π‘’)(((normCVβ€˜π‘’)β€˜π‘§) ≀ 1 ∧ π‘₯ = ((normCVβ€˜π‘€)β€˜(π‘‘β€˜π‘§)))}, ℝ*, < )))
361, 35wceq 1542 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  30046
  Copyright terms: Public domain W3C validator