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

Definition df-nmoo 22199
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 22195 . 2  class  normOp OLD
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 22016 . . 3  class  NrmCVec
5 vt . . . 4  set  t
63cv 1648 . . . . . 6  class  w
7 cba 22018 . . . . . 6  class  BaseSet
86, 7cfv 5413 . . . . 5  class  ( BaseSet `  w )
92cv 1648 . . . . . 6  class  u
109, 7cfv 5413 . . . . 5  class  ( BaseSet `  u )
11 cmap 6977 . . . . 5  class  ^m
128, 10, 11co 6040 . . . 4  class  ( (
BaseSet `  w )  ^m  ( BaseSet `  u )
)
13 vz . . . . . . . . . . 11  set  z
1413cv 1648 . . . . . . . . . 10  class  z
15 cnmcv 22022 . . . . . . . . . . 11  class  normCV
169, 15cfv 5413 . . . . . . . . . 10  class  ( normCV `  u )
1714, 16cfv 5413 . . . . . . . . 9  class  ( (
normCV
`  u ) `  z )
18 c1 8947 . . . . . . . . 9  class  1
19 cle 9077 . . . . . . . . 9  class  <_
2017, 18, 19wbr 4172 . . . . . . . 8  wff  ( (
normCV
`  u ) `  z )  <_  1
21 vx . . . . . . . . . 10  set  x
2221cv 1648 . . . . . . . . 9  class  x
235cv 1648 . . . . . . . . . . 11  class  t
2414, 23cfv 5413 . . . . . . . . . 10  class  ( t `
 z )
256, 15cfv 5413 . . . . . . . . . 10  class  ( normCV `  w )
2624, 25cfv 5413 . . . . . . . . 9  class  ( (
normCV
`  w ) `  ( t `  z
) )
2722, 26wceq 1649 . . . . . . . 8  wff  x  =  ( ( normCV `  w
) `  ( t `  z ) )
2820, 27wa 359 . . . . . . 7  wff  ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) )
2928, 13, 10wrex 2667 . . . . . 6  wff  E. z  e.  ( BaseSet `  u )
( ( ( normCV `  u ) `  z
)  <_  1  /\  x  =  ( ( normCV `  w ) `  (
t `  z )
) )
3029, 21cab 2390 . . . . 5  class  { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) }
31 cxr 9075 . . . . 5  class  RR*
32 clt 9076 . . . . 5  class  <
3330, 31, 32csup 7403 . . . 4  class  sup ( { x  |  E. z  e.  ( BaseSet `  u ) ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) ) } ,  RR* ,  <  )
345, 12, 33cmpt 4226 . . 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 6042 . 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 1649 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  22216
  Copyright terms: Public domain W3C validator