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

Metamath Proof Explorer

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 )