Metamath Proof Explorer

Theorem nmobndi

Description: Two ways to express that an operator is bounded. (Contributed by NM, 11-Jan-2008) (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 nmobndi 
|- ( T : X --> Y -> ( ( N ` T ) e. RR <-> E. r e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) ) )

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 leid 
 |-  ( ( N ` T ) e. RR -> ( N ` T ) <_ ( N ` T ) )
9 breq2 
 |-  ( r = ( N ` T ) -> ( ( N ` T ) <_ r <-> ( N ` T ) <_ ( N ` T ) ) )
10 9 rspcev 
 |-  ( ( ( N ` T ) e. RR /\ ( N ` T ) <_ ( N ` T ) ) -> E. r e. RR ( N ` T ) <_ r )
11 8 10 mpdan 
 |-  ( ( N ` T ) e. RR -> E. r e. RR ( N ` T ) <_ r )
12 1 2 5 nmoxr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) e. RR* )
13 6 7 12 mp3an12 
 |-  ( T : X --> Y -> ( N ` T ) e. RR* )
14 13 adantr 
 |-  ( ( T : X --> Y /\ ( r e. RR /\ ( N ` T ) <_ r ) ) -> ( N ` T ) e. RR* )
15 simprl 
 |-  ( ( T : X --> Y /\ ( r e. RR /\ ( N ` T ) <_ r ) ) -> r e. RR )
16 1 2 5 nmogtmnf 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> -oo < ( N ` T ) )
17 6 7 16 mp3an12 
 |-  ( T : X --> Y -> -oo < ( N ` T ) )
18 17 adantr 
 |-  ( ( T : X --> Y /\ ( r e. RR /\ ( N ` T ) <_ r ) ) -> -oo < ( N ` T ) )
19 simprr 
 |-  ( ( T : X --> Y /\ ( r e. RR /\ ( N ` T ) <_ r ) ) -> ( N ` T ) <_ r )
20 xrre 
 |-  ( ( ( ( N ` T ) e. RR* /\ r e. RR ) /\ ( -oo < ( N ` T ) /\ ( N ` T ) <_ r ) ) -> ( N ` T ) e. RR )
21 14 15 18 19 20 syl22anc 
 |-  ( ( T : X --> Y /\ ( r e. RR /\ ( N ` T ) <_ r ) ) -> ( N ` T ) e. RR )
22 21 rexlimdvaa 
 |-  ( T : X --> Y -> ( E. r e. RR ( N ` T ) <_ r -> ( N ` T ) e. RR ) )
23 11 22 impbid2 
 |-  ( T : X --> Y -> ( ( N ` T ) e. RR <-> E. r e. RR ( N ` T ) <_ r ) )
24 rexr 
 |-  ( r e. RR -> r e. RR* )
25 1 2 3 4 5 6 7 nmoubi 
 |-  ( ( T : X --> Y /\ r e. RR* ) -> ( ( N ` T ) <_ r <-> A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) ) )
26 24 25 sylan2 
 |-  ( ( T : X --> Y /\ r e. RR ) -> ( ( N ` T ) <_ r <-> A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) ) )
27 26 rexbidva 
 |-  ( T : X --> Y -> ( E. r e. RR ( N ` T ) <_ r <-> E. r e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) ) )
28 23 27 bitrd 
 |-  ( T : X --> Y -> ( ( N ` T ) e. RR <-> E. r e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) ) )