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

Metamath Proof Explorer

Theorem nmcfnlbi

Description: A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nmcfnex.1 
|- T e. LinFn
nmcfnex.2 
|- T e. ContFn
Assertion nmcfnlbi 
|- ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )

Proof

Step Hyp Ref Expression
1 nmcfnex.1 
 |-  T e. LinFn
2 nmcfnex.2 
 |-  T e. ContFn
3 fveq2 
 |-  ( A = 0h -> ( T ` A ) = ( T ` 0h ) )
4 1 lnfn0i 
 |-  ( T ` 0h ) = 0
5 3 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 2 nmcfnexi 
 |-  ( 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 1 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 norm-i 
 |-  ( A e. ~H -> ( ( normh ` A ) = 0 <-> A = 0h ) )
28 27 notbid 
 |-  ( A e. ~H -> ( -. ( normh ` A ) = 0 <-> -. A = 0h ) )
29 28 biimpar 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> -. ( normh ` A ) = 0 )
30 29 neqned 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( normh ` A ) =/= 0 )
31 23 26 30 divrec2d 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) = ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) )
32 25 30 rereccld 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( 1 / ( normh ` A ) ) e. RR )
33 32 recnd 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( 1 / ( normh ` A ) ) e. CC )
34 simpl 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> A e. ~H )
35 1 lnfnmuli 
 |-  ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) )
36 33 34 35 syl2anc 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) )
37 36 fveq2d 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) = ( abs ` ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) ) )
38 20 adantr 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( T ` A ) e. CC )
39 33 38 absmuld 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( abs ` ( T ` A ) ) ) )
40 df-ne 
 |-  ( A =/= 0h <-> -. A = 0h )
41 normgt0 
 |-  ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
42 40 41 bitr3id 
 |-  ( A e. ~H -> ( -. A = 0h <-> 0 < ( normh ` A ) ) )
43 42 biimpa 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> 0 < ( normh ` A ) )
44 25 43 recgt0d 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> 0 < ( 1 / ( normh ` A ) ) )
45 0re 
 |-  0 e. RR
46 ltle 
 |-  ( ( 0 e. RR /\ ( 1 / ( normh ` A ) ) e. RR ) -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
47 45 46 mpan 
 |-  ( ( 1 / ( normh ` A ) ) e. RR -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
48 32 44 47 sylc 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> 0 <_ ( 1 / ( normh ` A ) ) )
49 32 48 absidd 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( 1 / ( normh ` A ) ) ) = ( 1 / ( normh ` A ) ) )
50 49 oveq1d 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( abs ` ( T ` A ) ) ) = ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) )
51 37 39 50 3eqtrrd 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) = ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
52 31 51 eqtrd 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) = ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
53 hvmulcl 
 |-  ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
54 33 34 53 syl2anc 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
55 normcl 
 |-  ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
56 54 55 syl 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
57 norm1 
 |-  ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )
58 40 57 sylan2br 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )
59 eqle 
 |-  ( ( ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
60 56 58 59 syl2anc 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
61 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 ) )
62 19 61 mp3an1 
 |-  ( ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
63 54 60 62 syl2anc 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
64 52 63 eqbrtrd 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) )
65 12 a1i 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( normfn ` T ) e. RR )
66 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 ) ) ) )
67 22 65 25 43 66 syl112anc 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) <-> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) )
68 64 67 mpbid 
 |-  ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
69 18 68 pm2.61dan 
 |-  ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )