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 ffvelcdm 
 |-  ( ( 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 ) ) )