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

Definition df-nmo 18211
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 18208 . 2  class  normOp
2 vs . . 3  set  s
3 vt . . 3  set  t
4 cngp 18094 . . 3  class NrmGrp
5 vf . . . 4  set  f
62cv 1627 . . . . 5  class  s
73cv 1627 . . . . 5  class  t
8 cghm 14674 . . . . 5  class  GrpHom
96, 7, 8co 5819 . . . 4  class  ( s 
GrpHom  t )
10 vx . . . . . . . . . . 11  set  x
1110cv 1627 . . . . . . . . . 10  class  x
125cv 1627 . . . . . . . . . 10  class  f
1311, 12cfv 5221 . . . . . . . . 9  class  ( f `
 x )
14 cnm 18093 . . . . . . . . . 10  class  norm
157, 14cfv 5221 . . . . . . . . 9  class  ( norm `  t )
1613, 15cfv 5221 . . . . . . . 8  class  ( (
norm `  t ) `  ( f `  x
) )
17 vr . . . . . . . . . 10  set  r
1817cv 1627 . . . . . . . . 9  class  r
196, 14cfv 5221 . . . . . . . . . 10  class  ( norm `  s )
2011, 19cfv 5221 . . . . . . . . 9  class  ( (
norm `  s ) `  x )
21 cmul 8737 . . . . . . . . 9  class  x.
2218, 20, 21co 5819 . . . . . . . 8  class  ( r  x.  ( ( norm `  s ) `  x
) )
23 cle 8863 . . . . . . . 8  class  <_
2416, 22, 23wbr 4024 . . . . . . 7  wff  ( (
norm `  t ) `  ( f `  x
) )  <_  (
r  x.  ( (
norm `  s ) `  x ) )
25 cbs 13142 . . . . . . . 8  class  Base
266, 25cfv 5221 . . . . . . 7  class  ( Base `  s )
2724, 10, 26wral 2544 . . . . . 6  wff  A. x  e.  ( Base `  s
) ( ( norm `  t ) `  (
f `  x )
)  <_  ( r  x.  ( ( norm `  s
) `  x )
)
28 cc0 8732 . . . . . . 7  class  0
29 cpnf 8859 . . . . . . 7  class  +oo
30 cico 10652 . . . . . . 7  class  [,)
3128, 29, 30co 5819 . . . . . 6  class  ( 0 [,)  +oo )
3227, 17, 31crab 2548 . . . . 5  class  { r  e.  ( 0 [,) 
+oo )  |  A. x  e.  ( Base `  s ) ( (
norm `  t ) `  ( f `  x
) )  <_  (
r  x.  ( (
norm `  s ) `  x ) ) }
33 cxr 8861 . . . . 5  class  RR*
34 clt 8862 . . . . . 6  class  <
3534ccnv 4687 . . . . 5  class  `'  <
3632, 33, 35csup 7188 . . . 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 4078 . . 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 5821 . 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 1628 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  18214  nmofval  18217
  Copyright terms: Public domain W3C validator