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

Proof

Step Hyp Ref Expression
1 nmbdfnlb.1 ⊢T∈LinFn∧normfn⁡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ℎ→normfn⁡T⁢normℎ⁡A=normfn⁡T⋅0
12 1 simpri ⊢normfn⁡T∈ℝ
13 12 recni ⊢normfn⁡T∈ℂ
14 13 mul01i ⊢normfn⁡T⋅0=0
15 11 14 eqtr2di ⊢A=0ℎ→0=normfn⁡T⁢normℎ⁡A
16 7 15 breqtrid ⊢A=0ℎ→0≤normfn⁡T⁢normℎ⁡A
17 6 16 eqbrtrd ⊢A=0ℎ→T⁡A≤normfn⁡T⁢normℎ⁡A
18 17 adantl ⊢A∈ℋ∧A=0ℎ→T⁡A≤normfn⁡T⁢normℎ⁡A
19 3 lnfnfi ⊢T:ℋ⟶ℂ
20 19 ffvelcdmi ⊢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⁡Anormℎ⁡A=1normℎ⁡A⁢T⁡A
30 25 28 rereccld ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A∈ℝ
31 30 recnd ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A∈ℂ
32 simpl ⊢A∈ℋ∧A≠0ℎ→A∈ℋ
33 3 lnfnmuli ⊢1normℎ⁡A∈ℂ∧A∈ℋ→T⁡1normℎ⁡A⋅ℎA=1normℎ⁡A⁢T⁡A
34 31 32 33 syl2anc ⊢A∈ℋ∧A≠0ℎ→T⁡1normℎ⁡A⋅ℎA=1normℎ⁡A⁢T⁡A
35 34 fveq2d ⊢A∈ℋ∧A≠0ℎ→T⁡1normℎ⁡A⋅ℎA=1normℎ⁡A⁢T⁡A
36 20 adantr ⊢A∈ℋ∧A≠0ℎ→T⁡A∈ℂ
37 31 36 absmuld ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⁢T⁡A=1normℎ⁡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<1normℎ⁡A
41 0re ⊢0∈ℝ
42 ltle ⊢0∈ℝ∧1normℎ⁡A∈ℝ→0<1normℎ⁡A→0≤1normℎ⁡A
43 41 42 mpan ⊢1normℎ⁡A∈ℝ→0<1normℎ⁡A→0≤1normℎ⁡A
44 30 40 43 sylc ⊢A∈ℋ∧A≠0ℎ→0≤1normℎ⁡A
45 30 44 absidd ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A=1normℎ⁡A
46 45 oveq1d ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⁢T⁡A=1normℎ⁡A⁢T⁡A
47 35 37 46 3eqtrrd ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⁢T⁡A=T⁡1normℎ⁡A⋅ℎA
48 29 47 eqtrd ⊢A∈ℋ∧A≠0ℎ→T⁡Anormℎ⁡A=T⁡1normℎ⁡A⋅ℎA
49 hvmulcl ⊢1normℎ⁡A∈ℂ∧A∈ℋ→1normℎ⁡A⋅ℎA∈ℋ
50 31 32 49 syl2anc ⊢A∈ℋ∧A≠0ℎ→1normℎ⁡A⋅ℎA∈ℋ
51 normcl ⊢1normℎ⁡A⋅ℎA∈ℋ→normℎ⁡1normℎ⁡A⋅ℎA∈ℝ
52 50 51 syl ⊢A∈ℋ∧A≠0ℎ→normℎ⁡1normℎ⁡A⋅ℎA∈ℝ
53 norm1 ⊢A∈ℋ∧A≠0ℎ→normℎ⁡1normℎ⁡A⋅ℎA=1
54 eqle ⊢normℎ⁡1normℎ⁡A⋅ℎA∈ℝ∧normℎ⁡1normℎ⁡A⋅ℎA=1→normℎ⁡1normℎ⁡A⋅ℎA≤1
55 52 53 54 syl2anc ⊢A∈ℋ∧A≠0ℎ→normℎ⁡1normℎ⁡A⋅ℎA≤1
56 nmfnlb ⊢T:ℋ⟶ℂ∧1normℎ⁡A⋅ℎA∈ℋ∧normℎ⁡1normℎ⁡A⋅ℎA≤1→T⁡1normℎ⁡A⋅ℎA≤normfn⁡T
57 19 56 mp3an1 ⊢1normℎ⁡A⋅ℎA∈ℋ∧normℎ⁡1normℎ⁡A⋅ℎA≤1→T⁡1normℎ⁡A⋅ℎA≤normfn⁡T
58 50 55 57 syl2anc ⊢A∈ℋ∧A≠0ℎ→T⁡1normℎ⁡A⋅ℎA≤normfn⁡T
59 48 58 eqbrtrd ⊢A∈ℋ∧A≠0ℎ→T⁡Anormℎ⁡A≤normfn⁡T
60 12 a1i ⊢A∈ℋ∧A≠0ℎ→normfn⁡T∈ℝ
61 ledivmul2 ⊢T⁡A∈ℝ∧normfn⁡T∈ℝ∧normℎ⁡A∈ℝ∧0<normℎ⁡A→T⁡Anormℎ⁡A≤normfn⁡T↔T⁡A≤normfn⁡T⁢normℎ⁡A
62 22 60 25 39 61 syl112anc ⊢A∈ℋ∧A≠0ℎ→T⁡Anormℎ⁡A≤normfn⁡T↔T⁡A≤normfn⁡T⁢normℎ⁡A
63 59 62 mpbid ⊢A∈ℋ∧A≠0ℎ→T⁡A≤normfn⁡T⁢normℎ⁡A
64 18 63 pm2.61dane ⊢A∈ℋ→T⁡A≤normfn⁡T⁢normℎ⁡A