Metamath Proof Explorer

Theorem nmbdfnlb

Description: A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion nmbdfnlb ⊢T∈LinFn∧normfn⁡T∈ℝ∧A∈ℋ→T⁡A≤normfn⁡T⁢normℎ⁡A

Proof

Step Hyp Ref Expression
1 fveq1 ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→T⁡A=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁡A
2 1 fveq2d ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→T⁡A=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁡A
3 fveq2 ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→normfn⁡T=normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0
4 3 oveq1d ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→normfn⁡T⁢normℎ⁡A=normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁢normℎ⁡A
5 2 4 breq12d ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→T⁡A≤normfn⁡T⁢normℎ⁡A↔ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁡A≤normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁢normℎ⁡A
6 5 imbi2d ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→A∈ℋ→T⁡A≤normfn⁡T⁢normℎ⁡A↔A∈ℋ→ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁡A≤normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁢normℎ⁡A
7 eleq1 ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→T∈LinFn↔ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈LinFn
8 3 eleq1d ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→normfn⁡T∈ℝ↔normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈ℝ
9 7 8 anbi12d ⊢T=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→T∈LinFn∧normfn⁡T∈ℝ↔ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈LinFn∧normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈ℝ
10 eleq1 ⊢ℋ×0=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→ℋ×0∈LinFn↔ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈LinFn
11 fveq2 ⊢ℋ×0=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→normfn⁡ℋ×0=normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0
12 11 eleq1d ⊢ℋ×0=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→normfn⁡ℋ×0∈ℝ↔normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈ℝ
13 10 12 anbi12d ⊢ℋ×0=ifT∈LinFn∧normfn⁡T∈ℝTℋ×0→ℋ×0∈LinFn∧normfn⁡ℋ×0∈ℝ↔ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈LinFn∧normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈ℝ
14 0lnfn ⊢ℋ×0∈LinFn
15 nmfn0 ⊢normfn⁡ℋ×0=0
16 0re ⊢0∈ℝ
17 15 16 eqeltri ⊢normfn⁡ℋ×0∈ℝ
18 14 17 pm3.2i ⊢ℋ×0∈LinFn∧normfn⁡ℋ×0∈ℝ
19 9 13 18 elimhyp ⊢ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈LinFn∧normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0∈ℝ
20 19 nmbdfnlbi ⊢A∈ℋ→ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁡A≤normfn⁡ifT∈LinFn∧normfn⁡T∈ℝTℋ×0⁢normℎ⁡A
21 6 20 dedth ⊢T∈LinFn∧normfn⁡T∈ℝ→A∈ℋ→T⁡A≤normfn⁡T⁢normℎ⁡A
22 21 3impia ⊢T∈LinFn∧normfn⁡T∈ℝ∧A∈ℋ→T⁡A≤normfn⁡T⁢normℎ⁡A