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

Definition df-nmoo 25787
 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 CV CV
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-nmoo
StepHypRef Expression
1 cnmoo 25783 . 2
2 vu . . 3
3 vw . . 3
4 cnv 25604 . . 3
5 vt . . . 4
63cv 1394 . . . . . 6
7 cba 25606 . . . . . 6
86, 7cfv 5594 . . . . 5
92cv 1394 . . . . . 6
109, 7cfv 5594 . . . . 5
11 cmap 7438 . . . . 5
128, 10, 11co 6296 . . . 4
13 vz . . . . . . . . . . 11
1413cv 1394 . . . . . . . . . 10
15 cnmcv 25610 . . . . . . . . . . 11 CV
169, 15cfv 5594 . . . . . . . . . 10 CV
1714, 16cfv 5594 . . . . . . . . 9 CV
18 c1 9510 . . . . . . . . 9
19 cle 9646 . . . . . . . . 9
2017, 18, 19wbr 4456 . . . . . . . 8 CV
21 vx . . . . . . . . . 10
2221cv 1394 . . . . . . . . 9
235cv 1394 . . . . . . . . . . 11
2414, 23cfv 5594 . . . . . . . . . 10
256, 15cfv 5594 . . . . . . . . . 10 CV
2624, 25cfv 5594 . . . . . . . . 9 CV
2722, 26wceq 1395 . . . . . . . 8 CV
2820, 27wa 369 . . . . . . 7 CV CV
2928, 13, 10wrex 2808 . . . . . 6 CV CV
3029, 21cab 2442 . . . . 5 CV CV
31 cxr 9644 . . . . 5
32 clt 9645 . . . . 5
3330, 31, 32csup 7918 . . . 4 CV CV
345, 12, 33cmpt 4515 . . 3 CV CV
352, 3, 4, 4, 34cmpt2 6298 . 2 CV CV
361, 35wceq 1395 1 CV CV
 Colors of variables: wff setvar class This definition is referenced by:  nmoofval  25804
 Copyright terms: Public domain W3C validator