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 ⊢ ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ )
Assertion nmbdfnlbi ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmbdfnlb.1 ⊢ ( 𝑇 ∈ LinFn ∧ ( normfn ‘ 𝑇 ) ∈ ℝ )
2 fveq2 ⊢ ( 𝐴 = 0ℎ → ( 𝑇 ‘ 𝐴 ) = ( 𝑇 ‘ 0ℎ ) )
3 1 simpli ⊢ 𝑇 ∈ LinFn
4 3 lnfn0i ⊢ ( 𝑇 ‘ 0ℎ ) = 0
5 2 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 simpri ⊢ ( 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 3 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 normne0 ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0ℎ ) )
28 27 biimpar ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ 𝐴 ) ≠ 0 )
29 23 26 28 divrec2d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
30 25 28 rereccld ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ )
31 30 recnd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ )
32 simpl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 𝐴 ∈ ℋ )
33 3 lnfnmuli ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( 𝑇 ‘ 𝐴 ) ) )
34 31 32 33 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( 𝑇 ‘ 𝐴 ) ) )
35 34 fveq2d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) = ( abs ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( 𝑇 ‘ 𝐴 ) ) ) )
36 20 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( 𝑇 ‘ 𝐴 ) ∈ ℂ )
37 31 36 absmuld ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( abs ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( 𝑇 ‘ 𝐴 ) ) ) = ( ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
38 normgt0 ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ ↔ 0 < ( normℎ ‘ 𝐴 ) ) )
39 38 biimpa ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( normℎ ‘ 𝐴 ) )
40 25 39 recgt0d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) )
41 0re ⊢ 0 ∈ ℝ
42 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) ) )
43 41 42 mpan ⊢ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℝ → ( 0 < ( 1 / ( normℎ ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) ) )
44 30 40 43 sylc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 ≤ ( 1 / ( normℎ ‘ 𝐴 ) ) )
45 30 44 absidd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) = ( 1 / ( normℎ ‘ 𝐴 ) ) )
46 45 oveq1d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( abs ‘ ( 1 / ( normℎ ‘ 𝐴 ) ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
47 35 37 46 3eqtrrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) · ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ) = ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) )
48 29 47 eqtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) = ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) )
49 hvmulcl ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ )
50 31 32 49 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ )
51 normcl ⊢ ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ )
52 50 51 syl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ )
53 norm1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = 1 )
54 eqle ⊢ ( ( ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ∈ ℝ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) = 1 ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 )
55 52 53 54 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 )
56 nmfnlb ⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 ) → ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normfn ‘ 𝑇 ) )
57 19 56 mp3an1 ⊢ ( ( ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ∈ ℋ ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ≤ 1 ) → ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normfn ‘ 𝑇 ) )
58 50 55 57 syl2anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( abs ‘ ( 𝑇 ‘ ( ( 1 / ( normℎ ‘ 𝐴 ) ) ·ℎ 𝐴 ) ) ) ≤ ( normfn ‘ 𝑇 ) )
59 48 58 eqbrtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normfn ‘ 𝑇 ) )
60 12 a1i ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( normfn ‘ 𝑇 ) ∈ ℝ )
61 ledivmul2 ⊢ ( ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ ∧ ( normfn ‘ 𝑇 ) ∈ ℝ ∧ ( ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( normℎ ‘ 𝐴 ) ) ) → ( ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normfn ‘ 𝑇 ) ↔ ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
62 22 60 25 39 61 syl112anc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( ( ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) / ( normℎ ‘ 𝐴 ) ) ≤ ( normfn ‘ 𝑇 ) ↔ ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) ) )
63 59 62 mpbid ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
64 18 63 pm2.61dane ⊢ ( 𝐴 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )