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

Definition df-nmoo 21153
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 21149 . 2  class  normOp OLD
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 20970 . . 3  class  NrmCVec
5 vt . . . 4  set  t
63cv 1618 . . . . . 6  class  w
7 cba 20972 . . . . . 6  class  BaseSet
86, 7cfv 4592 . . . . 5  class  ( BaseSet `  w )
92cv 1618 . . . . . 6  class  u
109, 7cfv 4592 . . . . 5  class  ( BaseSet `  u )
11 cmap 6658 . . . . 5  class  ^m
128, 10, 11co 5710 . . . 4  class  ( (
BaseSet `  w )  ^m  ( BaseSet `  u )
)
13 vz . . . . . . . . . . 11  set  z
1413cv 1618 . . . . . . . . . 10  class  z
15 cnmcv 20976 . . . . . . . . . . 11  class  normCV
169, 15cfv 4592 . . . . . . . . . 10  class  ( normCV `  u )
1714, 16cfv 4592 . . . . . . . . 9  class  ( (
normCV
`  u ) `  z )
18 c1 8618 . . . . . . . . 9  class  1
19 cle 8748 . . . . . . . . 9  class  <_
2017, 18, 19wbr 3920 . . . . . . . 8  wff  ( (
normCV
`  u ) `  z )  <_  1
21 vx . . . . . . . . . 10  set  x
2221cv 1618 . . . . . . . . 9  class  x
235cv 1618 . . . . . . . . . . 11  class  t
2414, 23cfv 4592 . . . . . . . . . 10  class  ( t `
 z )
256, 15cfv 4592 . . . . . . . . . 10  class  ( normCV `  w )
2624, 25cfv 4592 . . . . . . . . 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 2510 . . . . . 6  wff  E. z  e.  ( BaseSet `  u )
( ( ( normCV `  u ) `  z
)  <_  1  /\  x  =  ( ( normCV `  w ) `  (
t `  z )
) )
3029, 21cab 2239 . . . . 5  class  { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) }
31 cxr 8746 . . . . 5  class  RR*
32 clt 8747 . . . . 5  class  <
3330, 31, 32csup 7077 . . . 4  class  sup ( { x  |  E. z  e.  ( BaseSet `  u ) ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) ) } ,  RR* ,  <  )
345, 12, 33cmpt 3974 . . 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 5712 . 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  21170
  Copyright terms: Public domain W3C validator