Theorem nmoub2i

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	nmoub2i	|- ( ( T : X --> Y /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ 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 6 7	nmoub3i	|- ( ( T : X --> Y /\ A e. RR /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ ( abs ` A ) )
9	8	3adant2r	|- ( ( T : X --> Y /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ ( abs ` A ) )
10		absid	|- ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
11	10	3ad2ant2	|- ( ( T : X --> Y /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( abs ` A ) = A )
12	9 11	breqtrd	|- ( ( T : X --> Y /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. X ( M ` ( T ` x ) ) <_ ( A x. ( L ` x ) ) ) -> ( N ` T ) <_ A )