This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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* , < ) ) )