This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmbdfnlbi

Description: A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmbdfnlb.1 
|- ( T e. LinFn /\ ( normfn ` T ) e. RR )
Assertion nmbdfnlbi 
|- ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 nmbdfnlb.1 
 |-  ( T e. LinFn /\ ( normfn ` T ) e. RR )
2 fveq2 
 |-  ( A = 0h -> ( T ` A ) = ( T ` 0h ) )
3 1 simpli 
 |-  T e. LinFn
4 3 lnfn0i 
 |-  ( T ` 0h ) = 0
5 2 4 eqtrdi 
 |-  ( A = 0h -> ( T ` A ) = 0 )
6 5 abs00bd 
 |-  ( A = 0h -> ( abs ` ( T ` A ) ) = 0 )
7 0le0 
 |-  0 <_ 0
8 fveq2 
 |-  ( A = 0h -> ( normh ` A ) = ( normh ` 0h ) )
9 norm0 
 |-  ( normh ` 0h ) = 0
10 8 9 eqtrdi 
 |-  ( A = 0h -> ( normh ` A ) = 0 )
11 10 oveq2d 
 |-  ( A = 0h -> ( ( normfn ` T ) x. ( normh ` A ) ) = ( ( normfn ` T ) x. 0 ) )
12 1 simpri 
 |-  ( normfn ` T ) e. RR
13 12 recni 
 |-  ( normfn ` T ) e. CC
14 13 mul01i 
 |-  ( ( normfn ` T ) x. 0 ) = 0
15 11 14 eqtr2di 
 |-  ( A = 0h -> 0 = ( ( normfn ` T ) x. ( normh ` A ) ) )
16 7 15 breqtrid 
 |-  ( A = 0h -> 0 <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
17 6 16 eqbrtrd 
 |-  ( A = 0h -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
18 17 adantl 
 |-  ( ( A e. ~H /\ A = 0h ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
19 3 lnfnfi 
 |-  T : ~H --> CC
20 19 ffvelcdmi 
 |-  ( A e. ~H -> ( T ` A ) e. CC )
21 20 abscld 
 |-  ( A e. ~H -> ( abs ` ( T ` A ) ) e. RR )
22 21 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` A ) ) e. RR )
23 22 recnd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` A ) ) e. CC )
24 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
25 24 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. RR )
26 25 recnd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. CC )
27 normne0 
 |-  ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )
28 27 biimpar 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) =/= 0 )
29 23 26 28 divrec2d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) = ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) )
30 25 28 rereccld 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. RR )
31 30 recnd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. CC )
32 simpl 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> A e. ~H )
33 3 lnfnmuli 
 |-  ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) )
34 31 32 33 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) )
35 34 fveq2d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) = ( abs ` ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) ) )
36 20 adantr 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( T ` A ) e. CC )
37 31 36 absmuld 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( abs ` ( T ` A ) ) ) )
38 normgt0 
 |-  ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
39 38 biimpa 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( normh ` A ) )
40 25 39 recgt0d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( 1 / ( normh ` A ) ) )
41 0re 
 |-  0 e. RR
42 ltle 
 |-  ( ( 0 e. RR /\ ( 1 / ( normh ` A ) ) e. RR ) -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
43 41 42 mpan 
 |-  ( ( 1 / ( normh ` A ) ) e. RR -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
44 30 40 43 sylc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> 0 <_ ( 1 / ( normh ` A ) ) )
45 30 44 absidd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( 1 / ( normh ` A ) ) ) = ( 1 / ( normh ` A ) ) )
46 45 oveq1d 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( abs ` ( T ` A ) ) ) = ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) )
47 35 37 46 3eqtrrd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) = ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
48 29 47 eqtrd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) = ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
49 hvmulcl 
 |-  ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
50 31 32 49 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
51 normcl 
 |-  ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
52 50 51 syl 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
53 norm1 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )
54 eqle 
 |-  ( ( ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
55 52 53 54 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
56 nmfnlb 
 |-  ( ( T : ~H --> CC /\ ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
57 19 56 mp3an1 
 |-  ( ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
58 50 55 57 syl2anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
59 48 58 eqbrtrd 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) )
60 12 a1i 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normfn ` T ) e. RR )
61 ledivmul2 
 |-  ( ( ( abs ` ( T ` A ) ) e. RR /\ ( normfn ` T ) e. RR /\ ( ( normh ` A ) e. RR /\ 0 < ( normh ` A ) ) ) -> ( ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) <-> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) )
62 22 60 25 39 61 syl112anc 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) <-> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) )
63 59 62 mpbid 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
64 18 63 pm2.61dane 
 |-  ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )