Metamath Proof Explorer


Theorem nmoleub

Description: The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of F ( x ) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses nmofval.1
|- N = ( S normOp T )
nmoi.2
|- V = ( Base ` S )
nmoi.3
|- L = ( norm ` S )
nmoi.4
|- M = ( norm ` T )
nmoi2.z
|- .0. = ( 0g ` S )
nmoleub.1
|- ( ph -> S e. NrmGrp )
nmoleub.2
|- ( ph -> T e. NrmGrp )
nmoleub.3
|- ( ph -> F e. ( S GrpHom T ) )
nmoleub.4
|- ( ph -> A e. RR* )
nmoleub.5
|- ( ph -> 0 <_ A )
Assertion nmoleub
|- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1
 |-  N = ( S normOp T )
2 nmoi.2
 |-  V = ( Base ` S )
3 nmoi.3
 |-  L = ( norm ` S )
4 nmoi.4
 |-  M = ( norm ` T )
5 nmoi2.z
 |-  .0. = ( 0g ` S )
6 nmoleub.1
 |-  ( ph -> S e. NrmGrp )
7 nmoleub.2
 |-  ( ph -> T e. NrmGrp )
8 nmoleub.3
 |-  ( ph -> F e. ( S GrpHom T ) )
9 nmoleub.4
 |-  ( ph -> A e. RR* )
10 nmoleub.5
 |-  ( ph -> 0 <_ A )
11 7 ad2antrr
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> T e. NrmGrp )
12 eqid
 |-  ( Base ` T ) = ( Base ` T )
13 2 12 ghmf
 |-  ( F e. ( S GrpHom T ) -> F : V --> ( Base ` T ) )
14 8 13 syl
 |-  ( ph -> F : V --> ( Base ` T ) )
15 14 ad2antrr
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> F : V --> ( Base ` T ) )
16 simprl
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> x e. V )
17 ffvelrn
 |-  ( ( F : V --> ( Base ` T ) /\ x e. V ) -> ( F ` x ) e. ( Base ` T ) )
18 15 16 17 syl2anc
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( F ` x ) e. ( Base ` T ) )
19 12 4 nmcl
 |-  ( ( T e. NrmGrp /\ ( F ` x ) e. ( Base ` T ) ) -> ( M ` ( F ` x ) ) e. RR )
20 11 18 19 syl2anc
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( M ` ( F ` x ) ) e. RR )
21 6 adantr
 |-  ( ( ph /\ ( N ` F ) <_ A ) -> S e. NrmGrp )
22 2 3 5 nmrpcl
 |-  ( ( S e. NrmGrp /\ x e. V /\ x =/= .0. ) -> ( L ` x ) e. RR+ )
23 22 3expb
 |-  ( ( S e. NrmGrp /\ ( x e. V /\ x =/= .0. ) ) -> ( L ` x ) e. RR+ )
24 21 23 sylan
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( L ` x ) e. RR+ )
25 20 24 rerpdivcld
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) e. RR )
26 25 rexrd
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) e. RR* )
27 1 nmocl
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
28 6 7 8 27 syl3anc
 |-  ( ph -> ( N ` F ) e. RR* )
29 28 ad2antrr
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( N ` F ) e. RR* )
30 9 ad2antrr
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> A e. RR* )
31 6 7 8 3jca
 |-  ( ph -> ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) )
32 31 adantr
 |-  ( ( ph /\ ( N ` F ) <_ A ) -> ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) )
33 1 2 3 4 5 nmoi2
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ ( N ` F ) )
34 32 33 sylan
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ ( N ` F ) )
35 simplr
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( N ` F ) <_ A )
36 26 29 30 34 35 xrletrd
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A )
37 36 expr
 |-  ( ( ( ph /\ ( N ` F ) <_ A ) /\ x e. V ) -> ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) )
38 37 ralrimiva
 |-  ( ( ph /\ ( N ` F ) <_ A ) -> A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) )
39 0le0
 |-  0 <_ 0
40 simpllr
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> A e. RR )
41 40 recnd
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> A e. CC )
42 41 mul01d
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( A x. 0 ) = 0 )
43 39 42 breqtrrid
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> 0 <_ ( A x. 0 ) )
44 fveq2
 |-  ( x = .0. -> ( F ` x ) = ( F ` .0. ) )
45 8 ad2antrr
 |-  ( ( ( ph /\ A e. RR ) /\ x e. V ) -> F e. ( S GrpHom T ) )
46 eqid
 |-  ( 0g ` T ) = ( 0g ` T )
47 5 46 ghmid
 |-  ( F e. ( S GrpHom T ) -> ( F ` .0. ) = ( 0g ` T ) )
48 45 47 syl
 |-  ( ( ( ph /\ A e. RR ) /\ x e. V ) -> ( F ` .0. ) = ( 0g ` T ) )
49 44 48 sylan9eqr
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( F ` x ) = ( 0g ` T ) )
50 49 fveq2d
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( M ` ( F ` x ) ) = ( M ` ( 0g ` T ) ) )
51 7 ad3antrrr
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> T e. NrmGrp )
52 4 46 nm0
 |-  ( T e. NrmGrp -> ( M ` ( 0g ` T ) ) = 0 )
53 51 52 syl
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( M ` ( 0g ` T ) ) = 0 )
54 50 53 eqtrd
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( M ` ( F ` x ) ) = 0 )
55 fveq2
 |-  ( x = .0. -> ( L ` x ) = ( L ` .0. ) )
56 6 ad2antrr
 |-  ( ( ( ph /\ A e. RR ) /\ x e. V ) -> S e. NrmGrp )
57 3 5 nm0
 |-  ( S e. NrmGrp -> ( L ` .0. ) = 0 )
58 56 57 syl
 |-  ( ( ( ph /\ A e. RR ) /\ x e. V ) -> ( L ` .0. ) = 0 )
59 55 58 sylan9eqr
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( L ` x ) = 0 )
60 59 oveq2d
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( A x. ( L ` x ) ) = ( A x. 0 ) )
61 43 54 60 3brtr4d
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) )
62 61 a1d
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x = .0. ) -> ( ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) )
63 simpr
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x =/= .0. ) -> x =/= .0. )
64 7 ad2antrr
 |-  ( ( ( ph /\ A e. RR ) /\ x e. V ) -> T e. NrmGrp )
65 14 adantr
 |-  ( ( ph /\ A e. RR ) -> F : V --> ( Base ` T ) )
66 65 17 sylan
 |-  ( ( ( ph /\ A e. RR ) /\ x e. V ) -> ( F ` x ) e. ( Base ` T ) )
67 64 66 19 syl2anc
 |-  ( ( ( ph /\ A e. RR ) /\ x e. V ) -> ( M ` ( F ` x ) ) e. RR )
68 67 adantr
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x =/= .0. ) -> ( M ` ( F ` x ) ) e. RR )
69 simpllr
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x =/= .0. ) -> A e. RR )
70 6 adantr
 |-  ( ( ph /\ A e. RR ) -> S e. NrmGrp )
71 22 3expa
 |-  ( ( ( S e. NrmGrp /\ x e. V ) /\ x =/= .0. ) -> ( L ` x ) e. RR+ )
72 70 71 sylanl1
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x =/= .0. ) -> ( L ` x ) e. RR+ )
73 68 69 72 ledivmul2d
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x =/= .0. ) -> ( ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A <-> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) )
74 73 biimpd
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x =/= .0. ) -> ( ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) )
75 63 74 embantd
 |-  ( ( ( ( ph /\ A e. RR ) /\ x e. V ) /\ x =/= .0. ) -> ( ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) )
76 62 75 pm2.61dane
 |-  ( ( ( ph /\ A e. RR ) /\ x e. V ) -> ( ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) )
77 76 ralimdva
 |-  ( ( ph /\ A e. RR ) -> ( A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) -> A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) ) )
78 7 adantr
 |-  ( ( ph /\ A e. RR ) -> T e. NrmGrp )
79 8 adantr
 |-  ( ( ph /\ A e. RR ) -> F e. ( S GrpHom T ) )
80 simpr
 |-  ( ( ph /\ A e. RR ) -> A e. RR )
81 10 adantr
 |-  ( ( ph /\ A e. RR ) -> 0 <_ A )
82 1 2 3 4 nmolb
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR /\ 0 <_ A ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) )
83 70 78 79 80 81 82 syl311anc
 |-  ( ( ph /\ A e. RR ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) )
84 77 83 syld
 |-  ( ( ph /\ A e. RR ) -> ( A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) -> ( N ` F ) <_ A ) )
85 84 imp
 |-  ( ( ( ph /\ A e. RR ) /\ A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) -> ( N ` F ) <_ A )
86 85 an32s
 |-  ( ( ( ph /\ A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) /\ A e. RR ) -> ( N ` F ) <_ A )
87 28 ad2antrr
 |-  ( ( ( ph /\ A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) e. RR* )
88 pnfge
 |-  ( ( N ` F ) e. RR* -> ( N ` F ) <_ +oo )
89 87 88 syl
 |-  ( ( ( ph /\ A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) <_ +oo )
90 simpr
 |-  ( ( ( ph /\ A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) /\ A = +oo ) -> A = +oo )
91 89 90 breqtrrd
 |-  ( ( ( ph /\ A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) <_ A )
92 ge0nemnf
 |-  ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo )
93 9 10 92 syl2anc
 |-  ( ph -> A =/= -oo )
94 9 93 jca
 |-  ( ph -> ( A e. RR* /\ A =/= -oo ) )
95 xrnemnf
 |-  ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )
96 94 95 sylib
 |-  ( ph -> ( A e. RR \/ A = +oo ) )
97 96 adantr
 |-  ( ( ph /\ A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) -> ( A e. RR \/ A = +oo ) )
98 86 91 97 mpjaodan
 |-  ( ( ph /\ A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) -> ( N ` F ) <_ A )
99 38 98 impbida
 |-  ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( x =/= .0. -> ( ( M ` ( F ` x ) ) / ( L ` x ) ) <_ A ) ) )