Theorem blo3i

Description: Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isblo3i.1	|- X = ( BaseSet ` U )
	isblo3i.m	|- M = ( normCV ` U )
	isblo3i.n	|- N = ( normCV ` W )
	isblo3i.4	|- L = ( U LnOp W )
	isblo3i.5	|- B = ( U BLnOp W )
	isblo3i.u	|- U e. NrmCVec
	isblo3i.w	|- W e. NrmCVec
Assertion	blo3i	|- ( ( T e. L /\ A e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( A x. ( M ` y ) ) ) -> T e. B )

Proof

Step	Hyp	Ref	Expression
1		isblo3i.1	|- X = ( BaseSet ` U )
2		isblo3i.m	|- M = ( normCV ` U )
3		isblo3i.n	|- N = ( normCV ` W )
4		isblo3i.4	|- L = ( U LnOp W )
5		isblo3i.5	|- B = ( U BLnOp W )
6		isblo3i.u	|- U e. NrmCVec
7		isblo3i.w	|- W e. NrmCVec
8		oveq1	|- ( x = A -> ( x x. ( M ` y ) ) = ( A x. ( M ` y ) ) )
9	8	breq2d	|- ( x = A -> ( ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) <-> ( N ` ( T ` y ) ) <_ ( A x. ( M ` y ) ) ) )
10	9	ralbidv	|- ( x = A -> ( A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) <-> A. y e. X ( N ` ( T ` y ) ) <_ ( A x. ( M ` y ) ) ) )
11	10	rspcev	|- ( ( A e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( A x. ( M ` y ) ) ) -> E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) )
12	1 2 3 4 5 6 7	isblo3i	|- ( T e. B <-> ( T e. L /\ E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) )
13	12	biimpri	|- ( ( T e. L /\ E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> T e. B )
14	11 13	sylan2	|- ( ( T e. L /\ ( A e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( A x. ( M ` y ) ) ) ) -> T e. B )
15	14	3impb	|- ( ( T e. L /\ A e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( A x. ( M ` y ) ) ) -> T e. B )