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

Definition df-nmo 18049
Description: Define the norm of an operator between two normed groups (usually vector spaces). This definition produces an operator norm function for each pair of groups  <. s ,  t
>.. Equivalent to the definition of linear operator norm in [AkhiezerGlazman] p. 39. (Contributed by Mario Carneiro, 18-Oct-2015.)
Assertion
Ref Expression
df-nmo  |-  normOp  =  ( s  e. NrmGrp ,  t  e. NrmGrp  |->  ( f  e.  ( s  GrpHom  t )  |->  sup ( { r  e.  ( 0 [,)  +oo )  |  A. x  e.  ( Base `  s
) ( ( norm `  t ) `  (
f `  x )
)  <_  ( r  x.  ( ( norm `  s
) `  x )
) } ,  RR* ,  `'  <  ) ) )
Distinct variable group:    f, r, s, t, x

Detailed syntax breakdown of Definition df-nmo
StepHypRef Expression
1 cnmo 18046 . 2  class  normOp
2 vs . . 3  set  s
3 vt . . 3  set  t
4 cngp 17932 . . 3  class NrmGrp
5 vf . . . 4  set  f
62cv 1618 . . . . 5  class  s
73cv 1618 . . . . 5  class  t
8 cghm 14515 . . . . 5  class  GrpHom
96, 7, 8co 5710 . . . 4  class  ( s 
GrpHom  t )
10 vx . . . . . . . . . . 11  set  x
1110cv 1618 . . . . . . . . . 10  class  x
125cv 1618 . . . . . . . . . 10  class  f
1311, 12cfv 4592 . . . . . . . . 9  class  ( f `
 x )
14 cnm 17931 . . . . . . . . . 10  class  norm
157, 14cfv 4592 . . . . . . . . 9  class  ( norm `  t )
1613, 15cfv 4592 . . . . . . . 8  class  ( (
norm `  t ) `  ( f `  x
) )
17 vr . . . . . . . . . 10  set  r
1817cv 1618 . . . . . . . . 9  class  r
196, 14cfv 4592 . . . . . . . . . 10  class  ( norm `  s )
2011, 19cfv 4592 . . . . . . . . 9  class  ( (
norm `  s ) `  x )
21 cmul 8622 . . . . . . . . 9  class  x.
2218, 20, 21co 5710 . . . . . . . 8  class  ( r  x.  ( ( norm `  s ) `  x
) )
23 cle 8748 . . . . . . . 8  class  <_
2416, 22, 23wbr 3920 . . . . . . 7  wff  ( (
norm `  t ) `  ( f `  x
) )  <_  (
r  x.  ( (
norm `  s ) `  x ) )
25 cbs 13022 . . . . . . . 8  class  Base
266, 25cfv 4592 . . . . . . 7  class  ( Base `  s )
2724, 10, 26wral 2509 . . . . . 6  wff  A. x  e.  ( Base `  s
) ( ( norm `  t ) `  (
f `  x )
)  <_  ( r  x.  ( ( norm `  s
) `  x )
)
28 cc0 8617 . . . . . . 7  class  0
29 cpnf 8744 . . . . . . 7  class  +oo
30 cico 10536 . . . . . . 7  class  [,)
3128, 29, 30co 5710 . . . . . 6  class  ( 0 [,)  +oo )
3227, 17, 31crab 2512 . . . . 5  class  { r  e.  ( 0 [,) 
+oo )  |  A. x  e.  ( Base `  s ) ( (
norm `  t ) `  ( f `  x
) )  <_  (
r  x.  ( (
norm `  s ) `  x ) ) }
33 cxr 8746 . . . . 5  class  RR*
34 clt 8747 . . . . . 6  class  <
3534ccnv 4579 . . . . 5  class  `'  <
3632, 33, 35csup 7077 . . . 4  class  sup ( { r  e.  ( 0 [,)  +oo )  |  A. x  e.  (
Base `  s )
( ( norm `  t
) `  ( f `  x ) )  <_ 
( r  x.  (
( norm `  s ) `  x ) ) } ,  RR* ,  `'  <  )
375, 9, 36cmpt 3974 . . 3  class  ( f  e.  ( s  GrpHom  t )  |->  sup ( { r  e.  ( 0 [,) 
+oo )  |  A. x  e.  ( Base `  s ) ( (
norm `  t ) `  ( f `  x
) )  <_  (
r  x.  ( (
norm `  s ) `  x ) ) } ,  RR* ,  `'  <  ) )
382, 3, 4, 4, 37cmpt2 5712 . 2  class  ( s  e. NrmGrp ,  t  e. NrmGrp  |->  ( f  e.  ( s  GrpHom  t )  |->  sup ( { r  e.  ( 0 [,)  +oo )  |  A. x  e.  ( Base `  s
) ( ( norm `  t ) `  (
f `  x )
)  <_  ( r  x.  ( ( norm `  s
) `  x )
) } ,  RR* ,  `'  <  ) ) )
391, 38wceq 1619 1  wff  normOp  =  ( s  e. NrmGrp ,  t  e. NrmGrp  |->  ( f  e.  ( s  GrpHom  t )  |->  sup ( { r  e.  ( 0 [,)  +oo )  |  A. x  e.  ( Base `  s
) ( ( norm `  t ) `  (
f `  x )
)  <_  ( r  x.  ( ( norm `  s
) `  x )
) } ,  RR* ,  `'  <  ) ) )
Colors of variables: wff set class
This definition is referenced by:  nmoffn  18052  nmofval  18055
  Copyright terms: Public domain W3C validator