Metamath Proof Explorer

Theorem nmoolb

Description: A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoolb.1 
|- X = ( BaseSet ` U )
nmoolb.2 
|- Y = ( BaseSet ` W )
nmoolb.l 
|- L = ( normCV ` U )
nmoolb.m 
|- M = ( normCV ` W )
nmoolb.3 
|- N = ( U normOpOLD W )
Assertion nmoolb 
|- ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) /\ ( A e. X /\ ( L ` A ) <_ 1 ) ) -> ( M ` ( T ` A ) ) <_ ( N ` T ) )

Proof

Step Hyp Ref Expression
1 nmoolb.1 
 |-  X = ( BaseSet ` U )
2 nmoolb.2 
 |-  Y = ( BaseSet ` W )
3 nmoolb.l 
 |-  L = ( normCV ` U )
4 nmoolb.m 
 |-  M = ( normCV ` W )
5 nmoolb.3 
 |-  N = ( U normOpOLD W )
6 2 4 nmosetre 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } C_ RR )
7 ressxr 
 |-  RR C_ RR*
8 6 7 sstrdi 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } C_ RR* )
9 8 3adant1 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } C_ RR* )
10 fveq2 
 |-  ( y = A -> ( L ` y ) = ( L ` A ) )
11 10 breq1d 
 |-  ( y = A -> ( ( L ` y ) <_ 1 <-> ( L ` A ) <_ 1 ) )
12 2fveq3 
 |-  ( y = A -> ( M ` ( T ` y ) ) = ( M ` ( T ` A ) ) )
13 12 eqeq2d 
 |-  ( y = A -> ( ( M ` ( T ` A ) ) = ( M ` ( T ` y ) ) <-> ( M ` ( T ` A ) ) = ( M ` ( T ` A ) ) ) )
14 11 13 anbi12d 
 |-  ( y = A -> ( ( ( L ` y ) <_ 1 /\ ( M ` ( T ` A ) ) = ( M ` ( T ` y ) ) ) <-> ( ( L ` A ) <_ 1 /\ ( M ` ( T ` A ) ) = ( M ` ( T ` A ) ) ) ) )
15 eqid 
 |-  ( M ` ( T ` A ) ) = ( M ` ( T ` A ) )
16 15 biantru 
 |-  ( ( L ` A ) <_ 1 <-> ( ( L ` A ) <_ 1 /\ ( M ` ( T ` A ) ) = ( M ` ( T ` A ) ) ) )
17 14 16 bitr4di 
 |-  ( y = A -> ( ( ( L ` y ) <_ 1 /\ ( M ` ( T ` A ) ) = ( M ` ( T ` y ) ) ) <-> ( L ` A ) <_ 1 ) )
18 17 rspcev 
 |-  ( ( A e. X /\ ( L ` A ) <_ 1 ) -> E. y e. X ( ( L ` y ) <_ 1 /\ ( M ` ( T ` A ) ) = ( M ` ( T ` y ) ) ) )
19 fvex 
 |-  ( M ` ( T ` A ) ) e. _V
20 eqeq1 
 |-  ( x = ( M ` ( T ` A ) ) -> ( x = ( M ` ( T ` y ) ) <-> ( M ` ( T ` A ) ) = ( M ` ( T ` y ) ) ) )
21 20 anbi2d 
 |-  ( x = ( M ` ( T ` A ) ) -> ( ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) <-> ( ( L ` y ) <_ 1 /\ ( M ` ( T ` A ) ) = ( M ` ( T ` y ) ) ) ) )
22 21 rexbidv 
 |-  ( x = ( M ` ( T ` A ) ) -> ( E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) <-> E. y e. X ( ( L ` y ) <_ 1 /\ ( M ` ( T ` A ) ) = ( M ` ( T ` y ) ) ) ) )
23 19 22 elab 
 |-  ( ( M ` ( T ` A ) ) e. { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } <-> E. y e. X ( ( L ` y ) <_ 1 /\ ( M ` ( T ` A ) ) = ( M ` ( T ` y ) ) ) )
24 18 23 sylibr 
 |-  ( ( A e. X /\ ( L ` A ) <_ 1 ) -> ( M ` ( T ` A ) ) e. { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } )
25 supxrub 
 |-  ( ( { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } C_ RR* /\ ( M ` ( T ` A ) ) e. { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } ) -> ( M ` ( T ` A ) ) <_ sup ( { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } , RR* , < ) )
26 9 24 25 syl2an 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) /\ ( A e. X /\ ( L ` A ) <_ 1 ) ) -> ( M ` ( T ` A ) ) <_ sup ( { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } , RR* , < ) )
27 1 2 3 4 5 nmooval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) = sup ( { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } , RR* , < ) )
28 27 adantr 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) /\ ( A e. X /\ ( L ` A ) <_ 1 ) ) -> ( N ` T ) = sup ( { x | E. y e. X ( ( L ` y ) <_ 1 /\ x = ( M ` ( T ` y ) ) ) } , RR* , < ) )
29 26 28 breqtrrd 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) /\ ( A e. X /\ ( L ` A ) <_ 1 ) ) -> ( M ` ( T ` A ) ) <_ ( N ` T ) )