# Metamath Proof Explorer

## Theorem nmoplb

Description: A lower bound for an operator norm. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 nmopsetretHIL ${⊢}{T}:ℋ⟶ℋ\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\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}={norm}_{ℎ}\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}={norm}_{ℎ}\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 {norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({T}\left({A}\right)\right)$
8 7 eqeq2d ${⊢}{y}={A}\to \left({norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)↔{norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({A}\right)\right)\right)$
9 6 8 anbi12d ${⊢}{y}={A}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({A}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({A}\right)\right)\right)\right)$
10 eqid ${⊢}{norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({A}\right)\right)$
11 10 biantru ${⊢}{norm}_{ℎ}\left({A}\right)\le 1↔\left({norm}_{ℎ}\left({A}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({A}\right)\right)\right)$
12 9 11 syl6bbr ${⊢}{y}={A}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\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 {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
14 fvex ${⊢}{norm}_{ℎ}\left({T}\left({A}\right)\right)\in \mathrm{V}$
15 eqeq1 ${⊢}{x}={norm}_{ℎ}\left({T}\left({A}\right)\right)\to \left({x}={norm}_{ℎ}\left({T}\left({y}\right)\right)↔{norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
16 15 anbi2d ${⊢}{x}={norm}_{ℎ}\left({T}\left({A}\right)\right)\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
17 16 rexbidv ${⊢}{x}={norm}_{ℎ}\left({T}\left({A}\right)\right)\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right)$
18 14 17 elab ${⊢}{norm}_{ℎ}\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}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {norm}_{ℎ}\left({T}\left({A}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)$
19 13 18 sylibr ${⊢}\left({A}\in ℋ\wedge {norm}_{ℎ}\left({A}\right)\le 1\right)\to {norm}_{ℎ}\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}={norm}_{ℎ}\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 {norm}_{ℎ}\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}={norm}_{ℎ}\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}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}\subseteq {ℝ}^{*}\wedge {norm}_{ℎ}\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}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}\right)\to {norm}_{ℎ}\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}={norm}_{ℎ}\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 {norm}_{ℎ}\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}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
23 nmopval ${⊢}{T}:ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\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{op}}\left({T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\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 {norm}_{ℎ}\left({T}\left({A}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)$