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 ⊢ T ∈ LinFn
nmcfnex.2 ⊢ T ∈ ContFn
Assertion nmcfnlbi ⊢ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 nmcfnex.1 ⊢ T ∈ LinFn
2 nmcfnex.2 ⊢ T ∈ ContFn
3 fveq2 ⊢ A = 0 ℎ → T ⁡ A = T ⁡ 0 ℎ
4 1 lnfn0i ⊢ T ⁡ 0 ℎ = 0
5 3 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 2 nmcfnexi ⊢ 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 1 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 norm-i ⊢ A ∈ ℋ → norm ℎ ⁡ A = 0 ↔ A = 0 ℎ
28 27 notbid ⊢ A ∈ ℋ → ¬ norm ℎ ⁡ A = 0 ↔ ¬ A = 0 ℎ
29 28 biimpar ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → ¬ norm ℎ ⁡ A = 0
30 29 neqned ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → norm ℎ ⁡ A ≠ 0
31 23 26 30 divrec2d ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ A norm ℎ ⁡ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A
32 25 30 rereccld ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 1 norm ℎ ⁡ A ∈ ℝ
33 32 recnd ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 1 norm ℎ ⁡ A ∈ ℂ
34 simpl ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → A ∈ ℋ
35 1 lnfnmuli ⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A
36 33 34 35 syl2anc ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A
37 36 fveq2d ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A
38 20 adantr ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ A ∈ ℂ
39 33 38 absmuld ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 1 norm ℎ ⁡ A ⁢ T ⁡ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A
40 df-ne ⊢ A ≠ 0 ℎ ↔ ¬ A = 0 ℎ
41 normgt0 ⊢ A ∈ ℋ → A ≠ 0 ℎ ↔ 0 < norm ℎ ⁡ A
42 40 41 bitr3id ⊢ A ∈ ℋ → ¬ A = 0 ℎ ↔ 0 < norm ℎ ⁡ A
43 42 biimpa ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 0 < norm ℎ ⁡ A
44 25 43 recgt0d ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 0 < 1 norm ℎ ⁡ A
45 0re ⊢ 0 ∈ ℝ
46 ltle ⊢ 0 ∈ ℝ ∧ 1 norm ℎ ⁡ A ∈ ℝ → 0 < 1 norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A
47 45 46 mpan ⊢ 1 norm ℎ ⁡ A ∈ ℝ → 0 < 1 norm ℎ ⁡ A → 0 ≤ 1 norm ℎ ⁡ A
48 32 44 47 sylc ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 0 ≤ 1 norm ℎ ⁡ A
49 32 48 absidd ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 1 norm ℎ ⁡ A = 1 norm ℎ ⁡ A
50 49 oveq1d ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 1 norm ℎ ⁡ A ⁢ T ⁡ A = 1 norm ℎ ⁡ A ⁢ T ⁡ A
51 37 39 50 3eqtrrd ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 1 norm ℎ ⁡ A ⁢ T ⁡ A = T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A
52 31 51 eqtrd ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ A norm ℎ ⁡ A = T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A
53 hvmulcl ⊢ 1 norm ℎ ⁡ A ∈ ℂ ∧ A ∈ ℋ → 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ
54 33 34 53 syl2anc ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ
55 normcl ⊢ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ
56 54 55 syl ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ
57 norm1 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1
58 40 57 sylan2br ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1
59 eqle ⊢ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℝ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A = 1 → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1
60 56 58 59 syl2anc ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1
61 nmfnlb ⊢ T : ℋ ⟶ ℂ ∧ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1 → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm fn ⁡ T
62 19 61 mp3an1 ⊢ 1 norm ℎ ⁡ A ⋅ ℎ A ∈ ℋ ∧ norm ℎ ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ 1 → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm fn ⁡ T
63 54 60 62 syl2anc ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ 1 norm ℎ ⁡ A ⋅ ℎ A ≤ norm fn ⁡ T
64 52 63 eqbrtrd ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ A norm ℎ ⁡ A ≤ norm fn ⁡ T
65 12 a1i ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → norm fn ⁡ T ∈ ℝ
66 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
67 22 65 25 43 66 syl112anc ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ A norm ℎ ⁡ A ≤ norm fn ⁡ T ↔ T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A
68 64 67 mpbid ⊢ A ∈ ℋ ∧ ¬ A = 0 ℎ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A
69 18 68 pm2.61dan ⊢ A ∈ ℋ → T ⁡ A ≤ norm fn ⁡ T ⁢ norm ℎ ⁡ A