Metamath Proof Explorer

Theorem nmopub

Description: An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopub 
|- ( ( T : ~H --> ~H /\ A e. RR* ) -> ( ( normop ` T ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )

Proof

Step Hyp Ref Expression
1 nmopval 
 |-  ( T : ~H --> ~H -> ( normop ` T ) = sup ( { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } , RR* , < ) )
2 1 adantr 
 |-  ( ( T : ~H --> ~H /\ A e. RR* ) -> ( normop ` T ) = sup ( { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } , RR* , < ) )
3 2 breq1d 
 |-  ( ( T : ~H --> ~H /\ A e. RR* ) -> ( ( normop ` T ) <_ A <-> sup ( { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } , RR* , < ) <_ A ) )
4 nmopsetretALT 
 |-  ( T : ~H --> ~H -> { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } C_ RR )
5 ressxr 
 |-  RR C_ RR*
6 4 5 sstrdi 
 |-  ( T : ~H --> ~H -> { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } C_ RR* )
7 supxrleub 
 |-  ( ( { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } C_ RR* /\ A e. RR* ) -> ( sup ( { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } , RR* , < ) <_ A <-> A. z e. { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } z <_ A ) )
8 6 7 sylan 
 |-  ( ( T : ~H --> ~H /\ A e. RR* ) -> ( sup ( { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } , RR* , < ) <_ A <-> A. z e. { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } z <_ A ) )
9 ancom 
 |-  ( ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) <-> ( y = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) )
10 eqeq1 
 |-  ( y = z -> ( y = ( normh ` ( T ` x ) ) <-> z = ( normh ` ( T ` x ) ) ) )
11 10 anbi1d 
 |-  ( y = z -> ( ( y = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) <-> ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) ) )
12 9 11 syl5bb 
 |-  ( y = z -> ( ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) <-> ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) ) )
13 12 rexbidv 
 |-  ( y = z -> ( E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) <-> E. x e. ~H ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) ) )
14 13 ralab 
 |-  ( A. z e. { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } z <_ A <-> A. z ( E. x e. ~H ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) )
15 ralcom4 
 |-  ( A. x e. ~H A. z ( ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) <-> A. z A. x e. ~H ( ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) )
16 impexp 
 |-  ( ( ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) <-> ( z = ( normh ` ( T ` x ) ) -> ( ( normh ` x ) <_ 1 -> z <_ A ) ) )
17 16 albii 
 |-  ( A. z ( ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) <-> A. z ( z = ( normh ` ( T ` x ) ) -> ( ( normh ` x ) <_ 1 -> z <_ A ) ) )
18 fvex 
 |-  ( normh ` ( T ` x ) ) e. _V
19 breq1 
 |-  ( z = ( normh ` ( T ` x ) ) -> ( z <_ A <-> ( normh ` ( T ` x ) ) <_ A ) )
20 19 imbi2d 
 |-  ( z = ( normh ` ( T ` x ) ) -> ( ( ( normh ` x ) <_ 1 -> z <_ A ) <-> ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )
21 18 20 ceqsalv 
 |-  ( A. z ( z = ( normh ` ( T ` x ) ) -> ( ( normh ` x ) <_ 1 -> z <_ A ) ) <-> ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) )
22 17 21 bitri 
 |-  ( A. z ( ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) <-> ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) )
23 22 ralbii 
 |-  ( A. x e. ~H A. z ( ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) )
24 r19.23v 
 |-  ( A. x e. ~H ( ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) <-> ( E. x e. ~H ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) )
25 24 albii 
 |-  ( A. z A. x e. ~H ( ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) <-> A. z ( E. x e. ~H ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) )
26 15 23 25 3bitr3i 
 |-  ( A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) <-> A. z ( E. x e. ~H ( z = ( normh ` ( T ` x ) ) /\ ( normh ` x ) <_ 1 ) -> z <_ A ) )
27 14 26 bitr4i 
 |-  ( A. z e. { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } z <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) )
28 8 27 bitrdi 
 |-  ( ( T : ~H --> ~H /\ A e. RR* ) -> ( sup ( { y | E. x e. ~H ( ( normh ` x ) <_ 1 /\ y = ( normh ` ( T ` x ) ) ) } , RR* , < ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )
29 3 28 bitrd 
 |-  ( ( T : ~H --> ~H /\ A e. RR* ) -> ( ( normop ` T ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )