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

Definition df-nmoo 25322
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  |-  normOpOLD  =  ( 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 25318 . 2  class  normOpOLD
2 vu . . 3  setvar  u
3 vw . . 3  setvar  w
4 cnv 25139 . . 3  class  NrmCVec
5 vt . . . 4  setvar  t
63cv 1373 . . . . . 6  class  w
7 cba 25141 . . . . . 6  class  BaseSet
86, 7cfv 5579 . . . . 5  class  ( BaseSet `  w )
92cv 1373 . . . . . 6  class  u
109, 7cfv 5579 . . . . 5  class  ( BaseSet `  u )
11 cmap 7410 . . . . 5  class  ^m
128, 10, 11co 6275 . . . 4  class  ( (
BaseSet `  w )  ^m  ( BaseSet `  u )
)
13 vz . . . . . . . . . . 11  setvar  z
1413cv 1373 . . . . . . . . . 10  class  z
15 cnmcv 25145 . . . . . . . . . . 11  class  normCV
169, 15cfv 5579 . . . . . . . . . 10  class  ( normCV `  u )
1714, 16cfv 5579 . . . . . . . . 9  class  ( (
normCV
`  u ) `  z )
18 c1 9482 . . . . . . . . 9  class  1
19 cle 9618 . . . . . . . . 9  class  <_
2017, 18, 19wbr 4440 . . . . . . . 8  wff  ( (
normCV
`  u ) `  z )  <_  1
21 vx . . . . . . . . . 10  setvar  x
2221cv 1373 . . . . . . . . 9  class  x
235cv 1373 . . . . . . . . . . 11  class  t
2414, 23cfv 5579 . . . . . . . . . 10  class  ( t `
 z )
256, 15cfv 5579 . . . . . . . . . 10  class  ( normCV `  w )
2624, 25cfv 5579 . . . . . . . . 9  class  ( (
normCV
`  w ) `  ( t `  z
) )
2722, 26wceq 1374 . . . . . . . 8  wff  x  =  ( ( normCV `  w
) `  ( t `  z ) )
2820, 27wa 369 . . . . . . 7  wff  ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) )
2928, 13, 10wrex 2808 . . . . . 6  wff  E. z  e.  ( BaseSet `  u )
( ( ( normCV `  u ) `  z
)  <_  1  /\  x  =  ( ( normCV `  w ) `  (
t `  z )
) )
3029, 21cab 2445 . . . . 5  class  { x  |  E. z  e.  (
BaseSet `  u ) ( ( ( normCV `  u
) `  z )  <_  1  /\  x  =  ( ( normCV `  w
) `  ( t `  z ) ) ) }
31 cxr 9616 . . . . 5  class  RR*
32 clt 9617 . . . . 5  class  <
3330, 31, 32csup 7889 . . . 4  class  sup ( { x  |  E. z  e.  ( BaseSet `  u ) ( ( ( normCV `  u ) `  z )  <_  1  /\  x  =  (
( normCV `  w ) `  ( t `  z
) ) ) } ,  RR* ,  <  )
345, 12, 33cmpt 4498 . . 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 6277 . 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 1374 1  wff  normOpOLD  =  ( 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 setvar class
This definition is referenced by:  nmoofval  25339
  Copyright terms: Public domain W3C validator