Metamath Proof Explorer

Theorem nmfnleub2

Description: An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 normcl 
 |-  ( x e. ~H -> ( normh ` x ) e. RR )
2 1 ad2antlr 
 |-  ( ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( normh ` x ) e. RR )
3 simpllr 
 |-  ( ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( A e. RR /\ 0 <_ A ) )
4 simpr 
 |-  ( ( ( ( T : ~H --> CC /\ ( 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 --> CC /\ ( 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 --> CC /\ ( A e. RR /\ 0 <_ A ) ) -> ( A x. 1 ) = A )
11 10 ad2antrr 
 |-  ( ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( A x. 1 ) = A )
12 8 11 breqtrd 
 |-  ( ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( A x. ( normh ` x ) ) <_ A )
13 ffvelrn 
 |-  ( ( T : ~H --> CC /\ x e. ~H ) -> ( T ` x ) e. CC )
14 13 abscld 
 |-  ( ( T : ~H --> CC /\ x e. ~H ) -> ( abs ` ( T ` x ) ) e. RR )
15 14 adantlr 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( abs ` ( T ` x ) ) e. RR )
16 remulcl 
 |-  ( ( A e. RR /\ ( normh ` x ) e. RR ) -> ( A x. ( normh ` x ) ) e. RR )
17 1 16 sylan2 
 |-  ( ( A e. RR /\ x e. ~H ) -> ( A x. ( normh ` x ) ) e. RR )
18 17 adantlr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ x e. ~H ) -> ( A x. ( normh ` x ) ) e. RR )
19 18 adantll 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( A x. ( normh ` x ) ) e. RR )
20 simplrl 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> A e. RR )
21 letr 
 |-  ( ( ( abs ` ( T ` x ) ) e. RR /\ ( A x. ( normh ` x ) ) e. RR /\ A e. RR ) -> ( ( ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) /\ ( A x. ( normh ` x ) ) <_ A ) -> ( abs ` ( T ` x ) ) <_ A ) )
22 15 19 20 21 syl3anc 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( ( ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) /\ ( A x. ( normh ` x ) ) <_ A ) -> ( abs ` ( T ` x ) ) <_ A ) )
23 22 adantr 
 |-  ( ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) /\ ( A x. ( normh ` x ) ) <_ A ) -> ( abs ` ( T ` x ) ) <_ A ) )
24 12 23 mpan2d 
 |-  ( ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) /\ ( normh ` x ) <_ 1 ) -> ( ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) -> ( abs ` ( T ` x ) ) <_ A ) )
25 24 ex 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( ( normh ` x ) <_ 1 -> ( ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) -> ( abs ` ( T ` x ) ) <_ A ) ) )
26 25 com23 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ x e. ~H ) -> ( ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) -> ( ( normh ` x ) <_ 1 -> ( abs ` ( T ` x ) ) <_ A ) ) )
27 26 ralimdva 
 |-  ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) -> ( A. x e. ~H ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) -> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( abs ` ( T ` x ) ) <_ A ) ) )
28 27 imp 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ A. x e. ~H ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( abs ` ( T ` x ) ) <_ A ) )
29 rexr 
 |-  ( A e. RR -> A e. RR* )
30 29 adantr 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A e. RR* )
31 nmfnleub 
 |-  ( ( T : ~H --> CC /\ A e. RR* ) -> ( ( normfn ` T ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( abs ` ( T ` x ) ) <_ A ) ) )
32 30 31 sylan2 
 |-  ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) -> ( ( normfn ` T ) <_ A <-> A. x e. ~H ( ( normh ` x ) <_ 1 -> ( abs ` ( T ` x ) ) <_ A ) ) )
33 32 biimpar 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ A. x e. ~H ( ( normh ` x ) <_ 1 -> ( abs ` ( T ` x ) ) <_ A ) ) -> ( normfn ` T ) <_ A )
34 28 33 syldan 
 |-  ( ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) ) /\ A. x e. ~H ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normfn ` T ) <_ A )
35 34 3impa 
 |-  ( ( T : ~H --> CC /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. ~H ( abs ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normfn ` T ) <_ A )