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

Definition df-nmoo 21323
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 21319 . 2  class  normOp OLD
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 21140 . . 3  class  NrmCVec
5 vt . . . 4  set  t
63cv 1622 . . . . . 6  class  w
7 cba 21142 . . . . . 6  class  BaseSet
86, 7cfv 5255 . . . . 5  class  ( BaseSet `  w )
92cv 1622 . . . . . 6  class  u
109, 7cfv 5255 . . . . 5  class  ( BaseSet `  u )
11 cmap 6772 . . . . 5  class  ^m
128, 10, 11co 5858 . . . 4  class  ( (
BaseSet `  w )  ^m  ( BaseSet `  u )
)
13 vz . . . . . . . . . . 11  set  z
1413cv 1622 . . . . . . . . . 10  class  z
15 cnmcv 21146 . . . . . . . . . . 11  class  normCV
169, 15cfv 5255 . . . . . . . . . 10  class  ( normCV `  u )
1714, 16cfv 5255 . . . . . . . . 9  class  ( (
normCV
`  u ) `  z )
18 c1 8738 . . . . . . . . 9  class  1
19 cle 8868 . . . . . . . . 9  class  <_
2017, 18, 19wbr 4023 . . . . . . . 8  wff  ( (
normCV
`  u ) `  z )  <_  1
21 vx . . . . . . . . . 10  set  x
2221cv 1622 . . . . . . . . 9  class  x
235cv 1622 . . . . . . . . . . 11  class  t
2414, 23cfv 5255 . . . . . . . . . 10  class  ( t `
 z )
256, 15cfv 5255 . . . . . . . . . 10  class  ( normCV `  w )
2624, 25cfv 5255 . . . . . . . . 9  class  ( (
normCV
`  w ) `  ( t `  z
) )
2722, 26wceq 1623 . . . . . . . 8  wff  x  =  ( ( normCV `  w
) `  ( t `  z ) )
2820, 27wa 358 . . . . . . 7  wff  ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) )
2928, 13, 10wrex 2544 . . . . . 6  wff  E. z  e.  ( BaseSet `  u )
( ( ( normCV `  u ) `  z
)  <_  1  /\  x  =  ( ( normCV `  w ) `  (
t `  z )
) )
3029, 21cab 2269 . . . . 5  class  { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) }
31 cxr 8866 . . . . 5  class  RR*
32 clt 8867 . . . . 5  class  <
3330, 31, 32csup 7193 . . . 4  class  sup ( { x  |  E. z  e.  ( BaseSet `  u ) ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) ) } ,  RR* ,  <  )
345, 12, 33cmpt 4077 . . 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 5860 . 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 1623 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  21340
  Copyright terms: Public domain W3C validator