# 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 ${⊢}\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\wedge {A}\in ℋ\right)\to \left|{T}\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right){norm}_{ℎ}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 fveq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to {T}\left({A}\right)=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\left({A}\right)$
2 1 fveq2d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left|{T}\left({A}\right)\right|=\left|if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\left({A}\right)\right|$
3 fveq2 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to {norm}_{\mathrm{fn}}\left({T}\right)={norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right)$
4 3 oveq1d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to {norm}_{\mathrm{fn}}\left({T}\right){norm}_{ℎ}\left({A}\right)={norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right){norm}_{ℎ}\left({A}\right)$
5 2 4 breq12d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left(\left|{T}\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right){norm}_{ℎ}\left({A}\right)↔\left|if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right){norm}_{ℎ}\left({A}\right)\right)$
6 5 imbi2d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left(\left({A}\in ℋ\to \left|{T}\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right){norm}_{ℎ}\left({A}\right)\right)↔\left({A}\in ℋ\to \left|if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right){norm}_{ℎ}\left({A}\right)\right)\right)$
7 eleq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left({T}\in \mathrm{LinFn}↔if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\in \mathrm{LinFn}\right)$
8 3 eleq1d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left({norm}_{\mathrm{fn}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right)\in ℝ\right)$
9 7 8 anbi12d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right)↔\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right)\in ℝ\right)\right)$
10 eleq1 ${⊢}ℋ×\left\{0\right\}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left(ℋ×\left\{0\right\}\in \mathrm{LinFn}↔if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\in \mathrm{LinFn}\right)$
11 fveq2 ${⊢}ℋ×\left\{0\right\}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to {norm}_{\mathrm{fn}}\left(ℋ×\left\{0\right\}\right)={norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right)$
12 11 eleq1d ${⊢}ℋ×\left\{0\right\}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left({norm}_{\mathrm{fn}}\left(ℋ×\left\{0\right\}\right)\in ℝ↔{norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right)\in ℝ\right)$
13 10 12 anbi12d ${⊢}ℋ×\left\{0\right\}=if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\to \left(\left(ℋ×\left\{0\right\}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left(ℋ×\left\{0\right\}\right)\in ℝ\right)↔\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right)\in ℝ\right)\right)$
14 0lnfn ${⊢}ℋ×\left\{0\right\}\in \mathrm{LinFn}$
15 nmfn0 ${⊢}{norm}_{\mathrm{fn}}\left(ℋ×\left\{0\right\}\right)=0$
16 0re ${⊢}0\in ℝ$
17 15 16 eqeltri ${⊢}{norm}_{\mathrm{fn}}\left(ℋ×\left\{0\right\}\right)\in ℝ$
18 14 17 pm3.2i ${⊢}\left(ℋ×\left\{0\right\}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left(ℋ×\left\{0\right\}\right)\in ℝ\right)$
19 9 13 18 elimhyp ${⊢}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right)\in ℝ\right)$
20 19 nmbdfnlbi ${⊢}{A}\in ℋ\to \left|if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left(if\left(\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right),{T},ℋ×\left\{0\right\}\right)\right){norm}_{ℎ}\left({A}\right)$
21 6 20 dedth ${⊢}\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\right)\to \left({A}\in ℋ\to \left|{T}\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right){norm}_{ℎ}\left({A}\right)\right)$
22 21 3impia ${⊢}\left({T}\in \mathrm{LinFn}\wedge {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ\wedge {A}\in ℋ\right)\to \left|{T}\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right){norm}_{ℎ}\left({A}\right)$