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 ) ) )