# 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 ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ$
Assertion nmbdfnlbi $⊢ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A$

### Proof

Step Hyp Ref Expression
1 nmbdfnlb.1 $⊢ T ∈ LinFn ∧ norm fn ⁡ T ∈ ℝ$
2 fveq2 $⊢ A = 0 ℎ → T ⁡ A = T ⁡ 0 ℎ$
3 1 simpli $⊢ T ∈ LinFn$
4 3 lnfn0i $⊢ T ⁡ 0 ℎ = 0$
5 2 4 eqtrdi $⊢ A = 0 ℎ → T ⁡ A = 0$
6 5 abs00bd $⊢ A = 0 ℎ → T ⁡ A = 0$
7 0le0 $⊢ 0 ≤ 0$
8 fveq2 $⊢ A = 0 ℎ → norm ℎ ⁡ A = norm ℎ ⁡ 0 ℎ$
9 norm0 $⊢ norm ℎ ⁡ 0 ℎ = 0$
10 8 9 eqtrdi $⊢ A = 0 ℎ → norm ℎ ⁡ A = 0$
11 10 oveq2d $⊢ A = 0 ℎ → norm fn ⁡ T ⁢ norm ℎ ⁡ A = norm fn ⁡ T ⋅ 0$
12 1 simpri $⊢ norm fn ⁡ T ∈ ℝ$
13 12 recni $⊢ norm fn ⁡ T ∈ ℂ$
14 13 mul01i $⊢ norm fn ⁡ T ⋅ 0 = 0$
15 11 14 eqtr2di $⊢ A = 0 ℎ → 0 = norm fn ⁡ T ⁢ norm ℎ ⁡ A$
16 7 15 breqtrid $⊢ A = 0 ℎ → 0 ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A$
17 6 16 eqbrtrd $⊢ A = 0 ℎ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A$
18 17 adantl $⊢ A ∈ ℋ ∧ A = 0 ℎ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A$
19 3 lnfnfi $⊢ T : ℋ ⟶ ℂ$
20 19 ffvelrni $⊢ A ∈ ℋ → T ⁡ A ∈ ℂ$
21 20 abscld $⊢ A ∈ ℋ → T ⁡ A ∈ ℝ$
22 21 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A ∈ ℝ$
23 22 recnd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A ∈ ℂ$
24 normcl $⊢ A ∈ ℋ → norm ℎ ⁡ A ∈ ℝ$
25 24 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ ℝ$
26 25 recnd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ∈ ℂ$
27 normne0 $⊢ A ∈ ℋ → norm ℎ ⁡ A ≠ 0 ↔ A ≠ 0 ℎ$
28 27 biimpar $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ A ≠ 0$
29 23 26 28 divrec2d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A$
30 25 28 rereccld $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ∈ ℝ$
31 30 recnd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ∈ ℂ$
32 simpl $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → A ∈ ℋ$
33 3 lnfnmuli $⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A$
34 31 32 33 syl2anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A$
35 34 fveq2d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A$
36 20 adantr $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A ∈ ℂ$
37 31 36 absmuld $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ T ⁡ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A$
38 normgt0 $⊢ A ∈ ℋ → A ≠ 0 ℎ ↔ 0 < norm ℎ ⁡ A$
39 38 biimpa $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < norm ℎ ⁡ A$
40 25 39 recgt0d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < 1 norm ℎ ⁡ A$
41 0re $⊢ 0 ∈ ℝ$
42 ltle $⊢ 0 ∈ ℝ ∧ 1 norm ℎ ⁡ A ∈ ℝ → 0 < 1 norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A$
43 41 42 mpan $⊢ 1 norm ℎ ⁡ A ∈ ℝ → 0 < 1 norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A$
44 30 40 43 sylc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 ≤ 1 norm ℎ ⁡ A$
45 30 44 absidd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A = 1 norm ℎ ⁡ A$
46 45 oveq1d $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ T ⁡ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A$
47 35 37 46 3eqtrrd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⁢ T ⁡ A = T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A$
48 29 47 eqtrd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A norm ℎ ⁡ A = T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A$
49 hvmulcl $⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ → 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ$
50 31 32 49 syl2anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ$
51 normcl $⊢ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ$
52 50 51 syl $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ$
53 norm1 $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1$
54 eqle $⊢ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1$
55 52 53 54 syl2anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1$
56 nmfnlb $⊢ T : ℋ ⟶ ℂ ∧ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1 → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm fn ⁡ T$
57 19 56 mp3an1 $⊢ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1 → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm fn ⁡ T$
58 50 55 57 syl2anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm fn ⁡ T$
59 48 58 eqbrtrd $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A norm ℎ ⁡ A ≤ norm fn ⁡ T$
60 12 a1i $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm fn ⁡ T ∈ ℝ$
61 ledivmul2 $⊢ T ⁡ A ∈ ℝ ∧ norm fn ⁡ T ∈ ℝ ∧ norm ℎ ⁡ A ∈ ℝ ∧ 0 < norm ℎ ⁡ A → T ⁡ A norm ℎ ⁡ A ≤ norm fn ⁡ T ↔ T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A$
62 22 60 25 39 61 syl112anc $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A norm ℎ ⁡ A ≤ norm fn ⁡ T ↔ T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A$
63 59 62 mpbid $⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A$
64 18 63 pm2.61dane $⊢ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A$