Metamath Proof Explorer

Theorem nmopub2tALT

Description: An upper bound for an operator norm. (Contributed by NM, 12-Apr-2006) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
2 1 ad2antlr 
 |-  ( ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` x ) e. RR )
3 simpllr 
 |-  ( ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( A e. RR /\ 0 <_ A ) )
4 simpr 
 |-  ( ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` x ) <_ 1 )
5 1re 
 |-  1 e. RR
6 lemul2a 
 |-  ( ( ( ( normh ` x ) e. RR /\ 1 e. RR /\ ( A e. RR /\ 0 <_ A ) ) /\ ( normh ` x ) <_ 1 ) -> ( A x. ( normh ` x ) ) <_ ( A x. 1 ) )
7 5 6 mp3anl2 
 |-  ( ( ( ( normh ` x ) e. RR /\ ( A e. RR /\ 0 <_ A ) ) /\ ( normh ` x ) <_ 1 ) -> ( A x. ( normh ` x ) ) <_ ( A x. 1 ) )
8 2 3 4 7 syl21anc 
 |-  ( ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( A x. ( normh ` x ) ) <_ ( A x. 1 ) )
9 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
10 9 ad2antrl 
 |-  ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) -> ( A x. 1 ) = A )
11 10 ad2antrr 
 |-  ( ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( A x. 1 ) = A )
12 8 11 breqtrd 
 |-  ( ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( A x. ( normh ` x ) ) <_ A )
13 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
14 normcl 
 |-  ( ( T ` x ) e. ~H -> ( normh ` ( T ` x ) ) e. RR )
15 13 14 syl 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( normh ` ( T ` x ) ) e. RR )
16 15 adantlr 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( normh ` ( T ` x ) ) e. RR )
17 remulcl 
 |-  ( ( A e. RR /\ ( normh ` x ) e. RR ) -> ( A x. ( normh ` x ) ) e. RR )
18 1 17 sylan2 
 |-  ( ( A e. RR /\ x e. ~H ) -> ( A x. ( normh ` x ) ) e. RR )
19 18 adantlr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ x e. ~H ) -> ( A x. ( normh ` x ) ) e. RR )
20 19 adantll 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( A x. ( normh ` x ) ) e. RR )
21 simplrl 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> A e. RR )
22 letr 
 |-  ( ( ( normh ` ( T ` x ) ) e. RR /\ ( A x. ( normh ` x ) ) e. RR /\ A e. RR ) -> ( ( ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) /\ ( A x. ( normh ` x ) ) <_ A ) -> ( normh ` ( T ` x ) ) <_ A ) )
23 16 20 21 22 syl3anc 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( ( ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) /\ ( A x. ( normh ` x ) ) <_ A ) -> ( normh ` ( T ` x ) ) <_ A ) )
24 23 adantr 
 |-  ( ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) /\ ( A x. ( normh ` x ) ) <_ A ) -> ( normh ` ( T ` x ) ) <_ A ) )
25 12 24 mpan2d 
 |-  ( ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) -> ( normh ` ( T ` x ) ) <_ A ) )
26 25 ex 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( ( normh ` x ) <_ 1 -> ( ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) -> ( normh ` ( T ` x ) ) <_ A ) ) )
27 26 com23 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) -> ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )
28 27 ralimdva 
 |-  ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) -> ( A. x e. ~H ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) -> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )
29 28 imp 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ A. x e. ~H ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) )
30 rexr 
 |-  ( A e. RR -> A e. RR* )
31 30 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. RR* )
32 nmopub 
 |-  ( ( T : ~H --> ~H /\ A e. RR* ) -> ( ( normop ` T ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )
33 31 32 sylan2 
 |-  ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) -> ( ( normop ` T ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) )
34 33 biimpar 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ A. x e. ~H ( ( normh ` x ) <_ 1 -> ( normh ` ( T ` x ) ) <_ A ) ) -> ( normop ` T ) <_ A )
35 29 34 syldan 
 |-  ( ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) ) /\ A. x e. ~H ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normop ` T ) <_ A )
36 35 3impa 
 |-  ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. ~H ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normop ` T ) <_ A )