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