Metamath Proof Explorer

Theorem nmoubi

Description: An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 
|- X = ( BaseSet ` U )
nmoubi.y 
|- Y = ( BaseSet ` W )
nmoubi.l 
|- L = ( normCV ` U )
nmoubi.m 
|- M = ( normCV ` W )
nmoubi.3 
|- N = ( U normOpOLD W )
nmoubi.u 
|- U e. NrmCVec
nmoubi.w 
|- W e. NrmCVec
Assertion nmoubi 
|- ( ( T : X --> Y /\ A e. RR* ) -> ( ( N ` T ) <_ A <-> A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ A ) ) )

Proof

Step Hyp Ref Expression
1 nmoubi.1 
 |-  X = ( BaseSet ` U )
2 nmoubi.y 
 |-  Y = ( BaseSet ` W )
3 nmoubi.l 
 |-  L = ( normCV ` U )
4 nmoubi.m 
 |-  M = ( normCV ` W )
5 nmoubi.3 
 |-  N = ( U normOpOLD W )
6 nmoubi.u 
 |-  U e. NrmCVec
7 nmoubi.w 
 |-  W e. NrmCVec
8 1 2 3 4 5 nmooval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) = sup ( { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } , RR* , < ) )
9 6 7 8 mp3an12 
 |-  ( T : X --> Y -> ( N ` T ) = sup ( { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } , RR* , < ) )
10 9 breq1d 
 |-  ( T : X --> Y -> ( ( N ` T ) <_ A <-> sup ( { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } , RR* , < ) <_ A ) )
11 10 adantr 
 |-  ( ( T : X --> Y /\ A e. RR* ) -> ( ( N ` T ) <_ A <-> sup ( { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } , RR* , < ) <_ A ) )
12 2 4 nmosetre 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } C_ RR )
13 7 12 mpan 
 |-  ( T : X --> Y -> { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } C_ RR )
14 ressxr 
 |-  RR C_ RR*
15 13 14 sstrdi 
 |-  ( T : X --> Y -> { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } C_ RR* )
16 supxrleub 
 |-  ( ( { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } C_ RR* /\ A e. RR* ) -> ( sup ( { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } , RR* , < ) <_ A <-> A. z e. { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } z <_ A ) )
17 15 16 sylan 
 |-  ( ( T : X --> Y /\ A e. RR* ) -> ( sup ( { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } , RR* , < ) <_ A <-> A. z e. { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } z <_ A ) )
18 11 17 bitrd 
 |-  ( ( T : X --> Y /\ A e. RR* ) -> ( ( N ` T ) <_ A <-> A. z e. { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } z <_ A ) )
19 eqeq1 
 |-  ( y = z -> ( y = ( M ` ( T ` x ) ) <-> z = ( M ` ( T ` x ) ) ) )
20 19 anbi2d 
 |-  ( y = z -> ( ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) <-> ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) ) )
21 20 rexbidv 
 |-  ( y = z -> ( E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) <-> E. x e. X ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) ) )
22 21 ralab 
 |-  ( A. z e. { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } z <_ A <-> A. z ( E. x e. X ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) )
23 ralcom4 
 |-  ( A. x e. X A. z ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) <-> A. z A. x e. X ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) )
24 ancomst 
 |-  ( ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) <-> ( ( z = ( M ` ( T ` x ) ) /\ ( L ` x ) <_ 1 ) -> z <_ A ) )
25 impexp 
 |-  ( ( ( z = ( M ` ( T ` x ) ) /\ ( L ` x ) <_ 1 ) -> z <_ A ) <-> ( z = ( M ` ( T ` x ) ) -> ( ( L ` x ) <_ 1 -> z <_ A ) ) )
26 24 25 bitri 
 |-  ( ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) <-> ( z = ( M ` ( T ` x ) ) -> ( ( L ` x ) <_ 1 -> z <_ A ) ) )
27 26 albii 
 |-  ( A. z ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) <-> A. z ( z = ( M ` ( T ` x ) ) -> ( ( L ` x ) <_ 1 -> z <_ A ) ) )
28 fvex 
 |-  ( M ` ( T ` x ) ) e. _V
29 breq1 
 |-  ( z = ( M ` ( T ` x ) ) -> ( z <_ A <-> ( M ` ( T ` x ) ) <_ A ) )
30 29 imbi2d 
 |-  ( z = ( M ` ( T ` x ) ) -> ( ( ( L ` x ) <_ 1 -> z <_ A ) <-> ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ A ) ) )
31 28 30 ceqsalv 
 |-  ( A. z ( z = ( M ` ( T ` x ) ) -> ( ( L ` x ) <_ 1 -> z <_ A ) ) <-> ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ A ) )
32 27 31 bitri 
 |-  ( A. z ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) <-> ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ A ) )
33 32 ralbii 
 |-  ( A. x e. X A. z ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) <-> A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ A ) )
34 r19.23v 
 |-  ( A. x e. X ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) <-> ( E. x e. X ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) )
35 34 albii 
 |-  ( A. z A. x e. X ( ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) <-> A. z ( E. x e. X ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) )
36 23 33 35 3bitr3i 
 |-  ( A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ A ) <-> A. z ( E. x e. X ( ( L ` x ) <_ 1 /\ z = ( M ` ( T ` x ) ) ) -> z <_ A ) )
37 22 36 bitr4i 
 |-  ( A. z e. { y | E. x e. X ( ( L ` x ) <_ 1 /\ y = ( M ` ( T ` x ) ) ) } z <_ A <-> A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ A ) )
38 18 37 bitrdi 
 |-  ( ( T : X --> Y /\ A e. RR* ) -> ( ( N ` T ) <_ A <-> A. x e. X ( ( L ` x ) <_ 1 -> ( M ` ( T ` x ) ) <_ A ) ) )