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𝐴 ) ) )