# 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 ) ) )`
` |-  ( ( A e. ~H /\ A = 0h ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )`
19 3 lnfnfi
` |-  T : ~H --> CC`
20 19 ffvelrni
` |-  ( A e. ~H -> ( T ` A ) e. CC )`
21 20 abscld
` |-  ( A e. ~H -> ( abs ` ( T ` A ) ) e. RR )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) )`