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 NrmGrp T NrmGrp N = f S GrpHom T sup r 0 +∞ | x V M f x r L x * <

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 norm s x = r L x
17 12 16 breq12d s = S t = T norm t f x r norm s x M f x r L x
18 8 17 raleqbidv s = S t = T x Base s norm t f x r norm s x x V M f x r L x
19 18 rabbidv s = S t = T r 0 +∞ | x Base s norm t f x r norm s x = r 0 +∞ | x V M f x r L x
20 19 infeq1d s = S t = T sup r 0 +∞ | x Base s norm t f x r norm s x * < = sup r 0 +∞ | x V M f x r L x * <
21 5 20 mpteq12dv s = S t = T f s GrpHom t sup r 0 +∞ | x Base s norm t f x r norm s x * < = f S GrpHom T sup r 0 +∞ | x V M f x r L x * <
22 df-nmo normOp = s NrmGrp , t NrmGrp f s GrpHom t sup r 0 +∞ | x Base s norm t f x r norm s x * <
23 eqid f S GrpHom T sup r 0 +∞ | x V M f x r L x * < = f S GrpHom T sup r 0 +∞ | x V M f x r L x * <
24 ssrab2 r 0 +∞ | x V M f x r L x 0 +∞
25 icossxr 0 +∞ *
26 24 25 sstri r 0 +∞ | x V M f x r L x *
27 infxrcl r 0 +∞ | x V M f x r L x * sup r 0 +∞ | x V M f x r L x * < *
28 26 27 mp1i f S GrpHom T sup r 0 +∞ | x V M f x r L x * < *
29 23 28 fmpti f S GrpHom T sup r 0 +∞ | x V M f x r L x * < : S GrpHom T *
30 ovex S GrpHom T V
31 xrex * V
32 fex2 f S GrpHom T sup r 0 +∞ | x V M f x r L x * < : S GrpHom T * S GrpHom T V * V f S GrpHom T sup r 0 +∞ | x V M f x r L x * < V
33 29 30 31 32 mp3an f S GrpHom T sup r 0 +∞ | x V M f x r L x * < V
34 21 22 33 ovmpoa S NrmGrp T NrmGrp S normOp T = f S GrpHom T sup r 0 +∞ | x V M f x r L x * <
35 1 34 syl5eq S NrmGrp T NrmGrp N = f S GrpHom T sup r 0 +∞ | x V M f x r L x * <