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

Metamath Proof Explorer

Theorem nmblolbi

Proof