Metamath Proof Explorer

Theorem nmofval

Description: Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Revised by AV, 26-Sep-2020)

Ref Expression
Hypotheses nmofval.1 
|- N = ( S normOp T )
nmofval.2 
|- V = ( Base ` S )
nmofval.3 
|- L = ( norm ` S )
nmofval.4 
|- M = ( norm ` T )
Assertion nmofval 
|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 nmofval.2 
 |-  V = ( Base ` S )
3 nmofval.3 
 |-  L = ( norm ` S )
4 nmofval.4 
 |-  M = ( norm ` T )
5 oveq12 
 |-  ( ( s = S /\ t = T ) -> ( s GrpHom t ) = ( S GrpHom T ) )
6 simpl 
 |-  ( ( s = S /\ t = T ) -> s = S )
7 6 fveq2d 
 |-  ( ( s = S /\ t = T ) -> ( Base ` s ) = ( Base ` S ) )
8 7 2 eqtr4di 
 |-  ( ( s = S /\ t = T ) -> ( Base ` s ) = V )
9 simpr 
 |-  ( ( s = S /\ t = T ) -> t = T )
10 9 fveq2d 
 |-  ( ( s = S /\ t = T ) -> ( norm ` t ) = ( norm ` T ) )
11 10 4 eqtr4di 
 |-  ( ( s = S /\ t = T ) -> ( norm ` t ) = M )
12 11 fveq1d 
 |-  ( ( s = S /\ t = T ) -> ( ( norm ` t ) ` ( f ` x ) ) = ( M ` ( f ` x ) ) )
13 6 fveq2d 
 |-  ( ( s = S /\ t = T ) -> ( norm ` s ) = ( norm ` S ) )
14 13 3 eqtr4di 
 |-  ( ( s = S /\ t = T ) -> ( norm ` s ) = L )
15 14 fveq1d 
 |-  ( ( s = S /\ t = T ) -> ( ( norm ` s ) ` x ) = ( L ` x ) )
16 15 oveq2d 
 |-  ( ( s = S /\ t = T ) -> ( r x. ( ( norm ` s ) ` x ) ) = ( r x. ( L ` x ) ) )
17 12 16 breq12d 
 |-  ( ( s = S /\ t = T ) -> ( ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) <-> ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) ) )
18 8 17 raleqbidv 
 |-  ( ( s = S /\ t = T ) -> ( A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) <-> A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) ) )
19 18 rabbidv 
 |-  ( ( s = S /\ t = T ) -> { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } = { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } )
20 19 infeq1d 
 |-  ( ( s = S /\ t = T ) -> inf ( { r e. ( 0 [,) +oo ) | A. x e. ( Base ` s ) ( ( norm ` t ) ` ( f ` x ) ) <_ ( r x. ( ( norm ` s ) ` x ) ) } , RR* , < ) = inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )
21 5 20 mpteq12dv 
 |-  ( ( s = S /\ t = T ) -> ( 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* , < ) ) = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) )
22 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* , < ) ) )
23 eqid 
 |-  ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) )
24 ssrab2 
 |-  { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } C_ ( 0 [,) +oo )
25 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
26 24 25 sstri 
 |-  { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } C_ RR*
27 infxrcl 
 |-  ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } C_ RR* -> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) e. RR* )
28 26 27 mp1i 
 |-  ( f e. ( S GrpHom T ) -> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) e. RR* )
29 23 28 fmpti 
 |-  ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) : ( S GrpHom T ) --> RR*
30 ovex 
 |-  ( S GrpHom T ) e. _V
31 xrex 
 |-  RR* e. _V
32 fex2 
 |-  ( ( ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) : ( S GrpHom T ) --> RR* /\ ( S GrpHom T ) e. _V /\ RR* e. _V ) -> ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) e. _V )
33 29 30 31 32 mp3an 
 |-  ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) e. _V
34 21 22 33 ovmpoa 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( S normOp T ) = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) )
35 1 34 syl5eq 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N = ( f e. ( S GrpHom T ) |-> inf ( { r e. ( 0 [,) +oo ) | A. x e. V ( M ` ( f ` x ) ) <_ ( r x. ( L ` x ) ) } , RR* , < ) ) )