This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmblolbi

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmblolbi.1 
|- X = ( BaseSet ` U )
nmblolbi.4 
|- L = ( normCV ` U )
nmblolbi.5 
|- M = ( normCV ` W )
nmblolbi.6 
|- N = ( U normOpOLD W )
nmblolbi.7 
|- B = ( U BLnOp W )
nmblolbi.u 
|- U e. NrmCVec
nmblolbi.w 
|- W e. NrmCVec
Assertion nmblolbi 
|- ( ( T e. B /\ A e. X ) -> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) )

Proof

Step Hyp Ref Expression
1 nmblolbi.1 
 |-  X = ( BaseSet ` U )
2 nmblolbi.4 
 |-  L = ( normCV ` U )
3 nmblolbi.5 
 |-  M = ( normCV ` W )
4 nmblolbi.6 
 |-  N = ( U normOpOLD W )
5 nmblolbi.7 
 |-  B = ( U BLnOp W )
6 nmblolbi.u 
 |-  U e. NrmCVec
7 nmblolbi.w 
 |-  W e. NrmCVec
8 fveq1 
 |-  ( T = if ( T e. B , T , ( U 0op W ) ) -> ( T ` A ) = ( if ( T e. B , T , ( U 0op W ) ) ` A ) )
9 8 fveq2d 
 |-  ( T = if ( T e. B , T , ( U 0op W ) ) -> ( M ` ( T ` A ) ) = ( M ` ( if ( T e. B , T , ( U 0op W ) ) ` A ) ) )
10 fveq2 
 |-  ( T = if ( T e. B , T , ( U 0op W ) ) -> ( N ` T ) = ( N ` if ( T e. B , T , ( U 0op W ) ) ) )
11 10 oveq1d 
 |-  ( T = if ( T e. B , T , ( U 0op W ) ) -> ( ( N ` T ) x. ( L ` A ) ) = ( ( N ` if ( T e. B , T , ( U 0op W ) ) ) x. ( L ` A ) ) )
12 9 11 breq12d 
 |-  ( T = if ( T e. B , T , ( U 0op W ) ) -> ( ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) <-> ( M ` ( if ( T e. B , T , ( U 0op W ) ) ` A ) ) <_ ( ( N ` if ( T e. B , T , ( U 0op W ) ) ) x. ( L ` A ) ) ) )
13 12 imbi2d 
 |-  ( T = if ( T e. B , T , ( U 0op W ) ) -> ( ( A e. X -> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) ) <-> ( A e. X -> ( M ` ( if ( T e. B , T , ( U 0op W ) ) ` A ) ) <_ ( ( N ` if ( T e. B , T , ( U 0op W ) ) ) x. ( L ` A ) ) ) ) )
14 eqid 
 |-  ( U 0op W ) = ( U 0op W )
15 14 5 0blo 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( U 0op W ) e. B )
16 6 7 15 mp2an 
 |-  ( U 0op W ) e. B
17 16 elimel 
 |-  if ( T e. B , T , ( U 0op W ) ) e. B
18 1 2 3 4 5 6 7 17 nmblolbii 
 |-  ( A e. X -> ( M ` ( if ( T e. B , T , ( U 0op W ) ) ` A ) ) <_ ( ( N ` if ( T e. B , T , ( U 0op W ) ) ) x. ( L ` A ) ) )
19 13 18 dedth 
 |-  ( T e. B -> ( A e. X -> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) ) )
20 19 imp 
 |-  ( ( T e. B /\ A e. X ) -> ( M ` ( T ` A ) ) <_ ( ( N ` T ) x. ( L ` A ) ) )