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

Definition df-nmoo 21269
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 
<. u ,  w >.. 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  |-  normOp OLD  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  ( t  e.  ( ( BaseSet `  w
)  ^m  ( BaseSet `  u ) )  |->  sup ( { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) } ,  RR* ,  <  ) ) )
Distinct variable group:    u, t, w, x, z

Detailed syntax breakdown of Definition df-nmoo
StepHypRef Expression
1 cnmoo 21265 . 2  class  normOp OLD
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 21086 . . 3  class  NrmCVec
5 vt . . . 4  set  t
63cv 1618 . . . . . 6  class  w
7 cba 21088 . . . . . 6  class  BaseSet
86, 7cfv 4659 . . . . 5  class  ( BaseSet `  w )
92cv 1618 . . . . . 6  class  u
109, 7cfv 4659 . . . . 5  class  ( BaseSet `  u )
11 cmap 6726 . . . . 5  class  ^m
128, 10, 11co 5778 . . . 4  class  ( (
BaseSet `  w )  ^m  ( BaseSet `  u )
)
13 vz . . . . . . . . . . 11  set  z
1413cv 1618 . . . . . . . . . 10  class  z
15 cnmcv 21092 . . . . . . . . . . 11  class  normCV
169, 15cfv 4659 . . . . . . . . . 10  class  ( normCV `  u )
1714, 16cfv 4659 . . . . . . . . 9  class  ( (
normCV
`  u ) `  z )
18 c1 8692 . . . . . . . . 9  class  1
19 cle 8822 . . . . . . . . 9  class  <_
2017, 18, 19wbr 3983 . . . . . . . 8  wff  ( (
normCV
`  u ) `  z )  <_  1
21 vx . . . . . . . . . 10  set  x
2221cv 1618 . . . . . . . . 9  class  x
235cv 1618 . . . . . . . . . . 11  class  t
2414, 23cfv 4659 . . . . . . . . . 10  class  ( t `
 z )
256, 15cfv 4659 . . . . . . . . . 10  class  ( normCV `  w )
2624, 25cfv 4659 . . . . . . . . 9  class  ( (
normCV
`  w ) `  ( t `  z
) )
2722, 26wceq 1619 . . . . . . . 8  wff  x  =  ( ( normCV `  w
) `  ( t `  z ) )
2820, 27wa 360 . . . . . . 7  wff  ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) )
2928, 13, 10wrex 2517 . . . . . 6  wff  E. z  e.  ( BaseSet `  u )
( ( ( normCV `  u ) `  z
)  <_  1  /\  x  =  ( ( normCV `  w ) `  (
t `  z )
) )
3029, 21cab 2242 . . . . 5  class  { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) }
31 cxr 8820 . . . . 5  class  RR*
32 clt 8821 . . . . 5  class  <
3330, 31, 32csup 7147 . . . 4  class  sup ( { x  |  E. z  e.  ( BaseSet `  u ) ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) ) } ,  RR* ,  <  )
345, 12, 33cmpt 4037 . . 3  class  ( t  e.  ( ( BaseSet `  w )  ^m  ( BaseSet
`  u ) ) 
|->  sup ( { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) } ,  RR* ,  <  ) )
352, 3, 4, 4, 34cmpt2 5780 . 2  class  ( u  e.  NrmCVec ,  w  e.  NrmCVec 
|->  ( t  e.  ( ( BaseSet `  w )  ^m  ( BaseSet `  u )
)  |->  sup ( { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) } ,  RR* ,  <  ) ) )
361, 35wceq 1619 1  wff  normOp OLD  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  ( t  e.  ( ( BaseSet `  w
)  ^m  ( BaseSet `  u ) )  |->  sup ( { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) } ,  RR* ,  <  ) ) )
Colors of variables: wff set class
This definition is referenced by:  nmoofval  21286
  Copyright terms: Public domain W3C validator