Metamath Proof Explorer

Theorem nmoplb

Description: A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nmopsetretHIL 
 |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )
2 ressxr 
 |-  RR C_ RR*
3 1 2 sstrdi 
 |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* )
4 3 3ad2ant1 
 |-  ( ( T : ~H --> ~H /\ A e. ~H /\ ( normh ` A ) <_ 1 ) -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* )
5 fveq2 
 |-  ( y = A -> ( normh ` y ) = ( normh ` A ) )
6 5 breq1d 
 |-  ( y = A -> ( ( normh ` y ) <_ 1 <-> ( normh ` A ) <_ 1 ) )
7 2fveq3 
 |-  ( y = A -> ( normh ` ( T ` y ) ) = ( normh ` ( T ` A ) ) )
8 7 eqeq2d 
 |-  ( y = A -> ( ( normh ` ( T ` A ) ) = ( normh ` ( T ` y ) ) <-> ( normh ` ( T ` A ) ) = ( normh ` ( T ` A ) ) ) )
9 6 8 anbi12d 
 |-  ( y = A -> ( ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` A ) ) = ( normh ` ( T ` y ) ) ) <-> ( ( normh ` A ) <_ 1 /\ ( normh ` ( T ` A ) ) = ( normh ` ( T ` A ) ) ) ) )
10 eqid 
 |-  ( normh ` ( T ` A ) ) = ( normh ` ( T ` A ) )
11 10 biantru 
 |-  ( ( normh ` A ) <_ 1 <-> ( ( normh ` A ) <_ 1 /\ ( normh ` ( T ` A ) ) = ( normh ` ( T ` A ) ) ) )
12 9 11 bitr4di 
 |-  ( y = A -> ( ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` A ) ) = ( normh ` ( T ` y ) ) ) <-> ( normh ` A ) <_ 1 ) )
13 12 rspcev 
 |-  ( ( A e. ~H /\ ( normh ` A ) <_ 1 ) -> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` A ) ) = ( normh ` ( T ` y ) ) ) )
14 fvex 
 |-  ( normh ` ( T ` A ) ) e. _V
15 eqeq1 
 |-  ( x = ( normh ` ( T ` A ) ) -> ( x = ( normh ` ( T ` y ) ) <-> ( normh ` ( T ` A ) ) = ( normh ` ( T ` y ) ) ) )
16 15 anbi2d 
 |-  ( x = ( normh ` ( T ` A ) ) -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` A ) ) = ( normh ` ( T ` y ) ) ) ) )
17 16 rexbidv 
 |-  ( x = ( normh ` ( T ` A ) ) -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` A ) ) = ( normh ` ( T ` y ) ) ) ) )
18 14 17 elab 
 |-  ( ( normh ` ( T ` A ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( normh ` ( T ` A ) ) = ( normh ` ( T ` y ) ) ) )
19 13 18 sylibr 
 |-  ( ( A e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normh ` ( T ` A ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } )
20 19 3adant1 
 |-  ( ( T : ~H --> ~H /\ A e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normh ` ( T ` A ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } )
21 supxrub 
 |-  ( ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR* /\ ( normh ` ( T ` A ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } ) -> ( normh ` ( T ` A ) ) <_ sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
22 4 20 21 syl2anc 
 |-  ( ( T : ~H --> ~H /\ A e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normh ` ( T ` A ) ) <_ sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
23 nmopval 
 |-  ( T : ~H --> ~H -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
24 23 3ad2ant1 
 |-  ( ( T : ~H --> ~H /\ A e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normop ` T ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } , RR* , < ) )
25 22 24 breqtrrd 
 |-  ( ( T : ~H --> ~H /\ A e. ~H /\ ( normh ` A ) <_ 1 ) -> ( normh ` ( T ` A ) ) <_ ( normop ` T ) )