Metamath Proof Explorer


Definition df-nmo

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) (Revised by AV, 25-Sep-2020)

Ref Expression
Assertion df-nmo
|- normOp = ( s e. NrmGrp , t e. NrmGrp |-> ( f e. ( s GrpHom t ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnmo
 |-  normOp
1 vs
 |-  s
2 cngp
 |-  NrmGrp
3 vt
 |-  t
4 vf
 |-  f
5 1 cv
 |-  s
6 cghm
 |-  GrpHom
7 3 cv
 |-  t
8 5 7 6 co
 |-  ( s GrpHom t )
9 vr
 |-  r
10 cc0
 |-  0
11 cico
 |-  [,)
12 cpnf
 |-  +oo
13 10 12 11 co
 |-  ( 0 [,) +oo )
14 vx
 |-  x
15 cbs
 |-  Base
16 5 15 cfv
 |-  ( Base ` s )
17 cnm
 |-  norm
18 7 17 cfv
 |-  ( norm ` t )
19 4 cv
 |-  f
20 14 cv
 |-  x
21 20 19 cfv
 |-  ( f ` x )
22 21 18 cfv
 |-  ( ( norm ` t ) ` ( f ` x ) )
23 cle
 |-  <_
24 9 cv
 |-  r
25 cmul
 |-  x.
26 5 17 cfv
 |-  ( norm ` s )
27 20 26 cfv
 |-  ( ( norm ` s ) ` x )
28 24 27 25 co
 |-  ( r x. ( ( norm ` s ) ` x ) )
29 22 28 23 wbr
 |-  ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) )
30 29 14 16 wral
 |-  A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) )
31 30 9 13 crab
 |-  { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) }
32 cxr
 |-  RR*
33 clt
 |-  <
34 31 32 33 cinf
 |-  inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < )
35 4 8 34 cmpt
 |-  ( f e. ( s GrpHom t ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) )
36 1 3 2 2 35 cmpo
 |-  ( s e. NrmGrp , t e. NrmGrp |-> ( f e. ( s GrpHom t ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) ) )
37 0 36 wceq
 |-  normOp = ( s e. NrmGrp , t e. NrmGrp |-> ( f e. ( s GrpHom t ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) ) )