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 ⊢ 𝑇 ∈ LinFn
nmcfnex.2 ⊢ 𝑇 ∈ ContFn
Assertion nmcfnlbi ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmcfnex.1 ⊢ 𝑇 ∈ LinFn
2 nmcfnex.2 ⊢ 𝑇 ∈ ContFn
3 fveq2 ⊢ ( 𝐴 = 0ℎ → ( 𝑇 ‘ 𝐴 ) = ( 𝑇 ‘ 0ℎ ) )
4 1 lnfn0i ⊢ ( 𝑇 ‘ 0ℎ ) = 0
5 3 4 eqtrdi ⊢ ( 𝐴 = 0ℎ → ( 𝑇 ‘ 𝐴 ) = 0 )
6 5 abs00bd ⊢ ( 𝐴 = 0ℎ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) = 0 )
7 0le0 ⊢ 0 ≤ 0
8 fveq2 ⊢ ( 𝐴 = 0ℎ → ( normℎ ‘ 𝐴 ) = ( normℎ ‘ 0ℎ ) )
9 norm0 ⊢ ( normℎ ‘ 0ℎ ) = 0
10 8 9 eqtrdi ⊢ ( 𝐴 = 0ℎ → ( normℎ ‘ 𝐴 ) = 0 )
11 10 oveq2d ⊢ ( 𝐴 = 0ℎ → ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) = ( ( normfn ‘ 𝑇 ) · 0 ) )
12 1 2 nmcfnexi ⊢ ( normfn ‘ 𝑇 ) ∈ ℝ
13 12 recni ⊢ ( normfn ‘ 𝑇 ) ∈ ℂ
14 13 mul01i ⊢ ( ( normfn ‘ 𝑇 ) · 0 ) = 0
15 11 14 eqtr2di ⊢ ( 𝐴 = 0ℎ → 0 = ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
16 7 15 breqtrid ⊢ ( 𝐴 = 0ℎ → 0 ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
17 6 16 eqbrtrd ⊢ ( 𝐴 = 0ℎ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
18 17 adantl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 = 0ℎ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
19 1 lnfnfi ⊢ 𝑇 : ℋ ⟶ ℂ
20 19 ffvelrni ⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℂ )
21 20 abscld ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
22 21 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
23 22 recnd ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℂ )
24 normcl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
25 24 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( normℎ ‘ 𝐴 ) ∈ ℝ )
26 25 recnd ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( normℎ ‘ 𝐴 ) ∈ ℂ )
27 norm-i ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0ℎ ) )
28 27 notbid ⊢ ( 𝐴 ∈ ℋ → ( ¬ ( normℎ ‘ 𝐴 ) = 0 ↔ ¬ 𝐴 = 0ℎ ) )
29 28 biimpar ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ¬ ( normℎ ‘ 𝐴 ) = 0 )
30 29 neqned ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( normℎ ‘ 𝐴 ) ≠ 0 )
31 23 26 30 divrec2d ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
32 25 30 rereccld ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ )
33 32 recnd ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ )
34 simpl ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → 𝐴 ∈ ℋ )
35 1 lnfnmuli ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( 𝑇 ‘ 𝐴 ) ) )
36 33 34 35 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( 𝑇 ‘ 𝐴 ) ) )
37 36 fveq2d ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) = ( abs ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( 𝑇 ‘ 𝐴 ) ) ) )
38 20 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℂ )
39 33 38 absmuld ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( abs ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( 𝑇 ‘ 𝐴 ) ) ) = ( ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
40 df-ne ⊢ ( 𝐴 ≠ 0ℎ ↔ ¬ 𝐴 = 0ℎ )
41 normgt0 ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ ↔ 0 < ( normℎ ‘ 𝐴 ) ) )
42 40 41 bitr3id ⊢ ( 𝐴 ∈ ℋ → ( ¬ 𝐴 = 0ℎ ↔ 0 < ( normℎ ‘ 𝐴 ) ) )
43 42 biimpa ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → 0 < ( normℎ ‘ 𝐴 ) )
44 25 43 recgt0d ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) )
45 0re ⊢ 0 ∈ ℝ
46 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) ) )
47 45 46 mpan ⊢ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ → ( 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) ) )
48 32 44 47 sylc ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) )
49 32 48 absidd ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) = ( 1 / ( normℎ ‘ 𝐴 ) ) )
50 49 oveq1d ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
51 37 39 50 3eqtrrd ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) = ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) )
52 31 51 eqtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) = ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) )
53 hvmulcl ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ )
54 33 34 53 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ )
55 normcl ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ )
56 54 55 syl ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ )
57 norm1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = 1 )
58 40 57 sylan2br ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = 1 )
59 eqle ⊢ ( ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = 1 ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 )
60 56 58 59 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 )
61 nmfnlb ⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 ) → ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normfn ‘ 𝑇 ) )
62 19 61 mp3an1 ⊢ ( ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 ) → ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normfn ‘ 𝑇 ) )
63 54 60 62 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normfn ‘ 𝑇 ) )
64 52 63 eqbrtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normfn ‘ 𝑇 ) )
65 12 a1i ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( normfn ‘ 𝑇 ) ∈ ℝ )
66 ledivmul2 ⊢ ( ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ∧ ( ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( normℎ ‘ 𝐴 ) ) ) → ( ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normfn ‘ 𝑇 ) ↔ ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
67 22 65 25 43 66 syl112anc ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normfn ‘ 𝑇 ) ↔ ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
68 64 67 mpbid ⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
69 18 68 pm2.61dan ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )