Metamath Proof Explorer

Theorem isblo3i

Description: The predicate "is a bounded linear operator." Definition 2.7-1 of Kreyszig p. 91. (Contributed by NM, 11-Dec-2007) (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 isblo3i 
|- ( T e. B <-> ( T e. L /\ E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) )

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 4 5 bloln 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T e. L )
9 6 7 8 mp3an12 
 |-  ( T e. B -> T e. L )
10 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
11 eqid 
 |-  ( U normOpOLD W ) = ( U normOpOLD W )
12 1 10 11 5 nmblore 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> ( ( U normOpOLD W ) ` T ) e. RR )
13 6 7 12 mp3an12 
 |-  ( T e. B -> ( ( U normOpOLD W ) ` T ) e. RR )
14 1 2 3 11 5 6 7 nmblolbi 
 |-  ( ( T e. B /\ y e. X ) -> ( N ` ( T ` y ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( M ` y ) ) )
15 14 ralrimiva 
 |-  ( T e. B -> A. y e. X ( N ` ( T ` y ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( M ` y ) ) )
16 oveq1 
 |-  ( x = ( ( U normOpOLD W ) ` T ) -> ( x x. ( M ` y ) ) = ( ( ( U normOpOLD W ) ` T ) x. ( M ` y ) ) )
17 16 breq2d 
 |-  ( x = ( ( U normOpOLD W ) ` T ) -> ( ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) <-> ( N ` ( T ` y ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( M ` y ) ) ) )
18 17 ralbidv 
 |-  ( x = ( ( U normOpOLD W ) ` T ) -> ( A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) <-> A. y e. X ( N ` ( T ` y ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( M ` y ) ) ) )
19 18 rspcev 
 |-  ( ( ( ( U normOpOLD W ) ` T ) e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( M ` y ) ) ) -> E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) )
20 13 15 19 syl2anc 
 |-  ( T e. B -> E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) )
21 9 20 jca 
 |-  ( T e. B -> ( T e. L /\ E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) )
22 simp1 
 |-  ( ( T e. L /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> T e. L )
23 1 10 4 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> ( BaseSet ` W ) )
24 6 7 23 mp3an12 
 |-  ( T e. L -> T : X --> ( BaseSet ` W ) )
25 1 10 11 nmoxr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> ( BaseSet ` W ) ) -> ( ( U normOpOLD W ) ` T ) e. RR* )
26 6 7 25 mp3an12 
 |-  ( T : X --> ( BaseSet ` W ) -> ( ( U normOpOLD W ) ` T ) e. RR* )
27 26 3ad2ant1 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> ( ( U normOpOLD W ) ` T ) e. RR* )
28 recn 
 |-  ( x e. RR -> x e. CC )
29 28 abscld 
 |-  ( x e. RR -> ( abs ` x ) e. RR )
30 29 rexrd 
 |-  ( x e. RR -> ( abs ` x ) e. RR* )
31 30 3ad2ant2 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> ( abs ` x ) e. RR* )
32 pnfxr 
 |-  +oo e. RR*
33 32 a1i 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> +oo e. RR* )
34 1 10 2 3 11 6 7 nmoub3i 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> ( ( U normOpOLD W ) ` T ) <_ ( abs ` x ) )
35 ltpnf 
 |-  ( ( abs ` x ) e. RR -> ( abs ` x ) < +oo )
36 29 35 syl 
 |-  ( x e. RR -> ( abs ` x ) < +oo )
37 36 3ad2ant2 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> ( abs ` x ) < +oo )
38 27 31 33 34 37 xrlelttrd 
 |-  ( ( T : X --> ( BaseSet ` W ) /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> ( ( U normOpOLD W ) ` T ) < +oo )
39 24 38 syl3an1 
 |-  ( ( T e. L /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> ( ( U normOpOLD W ) ` T ) < +oo )
40 11 4 5 isblo 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. B <-> ( T e. L /\ ( ( U normOpOLD W ) ` T ) < +oo ) ) )
41 6 7 40 mp2an 
 |-  ( T e. B <-> ( T e. L /\ ( ( U normOpOLD W ) ` T ) < +oo ) )
42 22 39 41 sylanbrc 
 |-  ( ( T e. L /\ x e. RR /\ A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> T e. B )
43 42 rexlimdv3a 
 |-  ( T e. L -> ( E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) -> T e. B ) )
44 43 imp 
 |-  ( ( T e. L /\ E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) -> T e. B )
45 21 44 impbii 
 |-  ( T e. B <-> ( T e. L /\ E. x e. RR A. y e. X ( N ` ( T ` y ) ) <_ ( x x. ( M ` y ) ) ) )