# Metamath Proof Explorer

## Theorem nmfnlb

Description: A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmfnlb ${⊢}\left({T}:ℋ⟶ℂ\wedge {A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{T}\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 nmfnsetre ${⊢}{T}:ℋ⟶ℂ\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}\subseteq ℝ$
2 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
3 1 2 sstrdi ${⊢}{T}:ℋ⟶ℂ\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}\subseteq {ℝ}^{*}$
4 3 3ad2ant1 ${⊢}\left({T}:ℋ⟶ℂ\wedge {A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}\subseteq {ℝ}^{*}$
5 fveq2 ${⊢}{y}={A}\to {norm}_{ℎ}\left({y}\right)={norm}_{ℎ}\left({A}\right)$
6 5 breq1d ${⊢}{y}={A}\to \left({norm}_{ℎ}\left({y}\right)\le 1↔{norm}_{ℎ}\left({A}\right)\le 1\right)$
7 2fveq3 ${⊢}{y}={A}\to \left|{T}\left({y}\right)\right|=\left|{T}\left({A}\right)\right|$
8 7 eqeq2d ${⊢}{y}={A}\to \left(\left|{T}\left({A}\right)\right|=\left|{T}\left({y}\right)\right|↔\left|{T}\left({A}\right)\right|=\left|{T}\left({A}\right)\right|\right)$
9 6 8 anbi12d ${⊢}{y}={A}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({A}\right)\right|=\left|{T}\left({y}\right)\right|\right)↔\left({norm}_{ℎ}\left({A}\right)\le 1\wedge \left|{T}\left({A}\right)\right|=\left|{T}\left({A}\right)\right|\right)\right)$
10 eqid ${⊢}\left|{T}\left({A}\right)\right|=\left|{T}\left({A}\right)\right|$
11 10 biantru ${⊢}{norm}_{ℎ}\left({A}\right)\le 1↔\left({norm}_{ℎ}\left({A}\right)\le 1\wedge \left|{T}\left({A}\right)\right|=\left|{T}\left({A}\right)\right|\right)$
12 9 11 syl6bbr ${⊢}{y}={A}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({A}\right)\right|=\left|{T}\left({y}\right)\right|\right)↔{norm}_{ℎ}\left({A}\right)\le 1\right)$
13 12 rspcev ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({A}\right)\right|=\left|{T}\left({y}\right)\right|\right)$
14 fvex ${⊢}\left|{T}\left({A}\right)\right|\in \mathrm{V}$
15 eqeq1 ${⊢}{x}=\left|{T}\left({A}\right)\right|\to \left({x}=\left|{T}\left({y}\right)\right|↔\left|{T}\left({A}\right)\right|=\left|{T}\left({y}\right)\right|\right)$
16 15 anbi2d ${⊢}{x}=\left|{T}\left({A}\right)\right|\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({A}\right)\right|=\left|{T}\left({y}\right)\right|\right)\right)$
17 16 rexbidv ${⊢}{x}=\left|{T}\left({A}\right)\right|\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({A}\right)\right|=\left|{T}\left({y}\right)\right|\right)\right)$
18 14 17 elab ${⊢}\left|{T}\left({A}\right)\right|\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge \left|{T}\left({A}\right)\right|=\left|{T}\left({y}\right)\right|\right)$
19 13 18 sylibr ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{T}\left({A}\right)\right|\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}$
20 19 3adant1 ${⊢}\left({T}:ℋ⟶ℂ\wedge {A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{T}\left({A}\right)\right|\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}$
21 supxrub ${⊢}\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}\subseteq {ℝ}^{*}\wedge \left|{T}\left({A}\right)\right|\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}\right)\to \left|{T}\left({A}\right)\right|\le sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\},{ℝ}^{*},<\right)$
22 4 20 21 syl2anc ${⊢}\left({T}:ℋ⟶ℂ\wedge {A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{T}\left({A}\right)\right|\le sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\},{ℝ}^{*},<\right)$
23 nmfnval ${⊢}{T}:ℋ⟶ℂ\to {norm}_{\mathrm{fn}}\left({T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\},{ℝ}^{*},<\right)$
24 23 3ad2ant1 ${⊢}\left({T}:ℋ⟶ℂ\wedge {A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{\mathrm{fn}}\left({T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\},{ℝ}^{*},<\right)$
25 22 24 breqtrrd ${⊢}\left({T}:ℋ⟶ℂ\wedge {A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to \left|{T}\left({A}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right)$