# Metamath Proof Explorer

## Theorem nmopub

Description: An upper bound for an operator norm. (Contributed by NM, 7-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopub ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in {ℝ}^{*}\right)\to \left({norm}_{\mathrm{op}}\left({T}\right)\le {A}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 nmopval ${⊢}{T}:ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({T}\right)=sup\left(\left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
2 1 adantr ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in {ℝ}^{*}\right)\to {norm}_{\mathrm{op}}\left({T}\right)=sup\left(\left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
3 2 breq1d ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in {ℝ}^{*}\right)\to \left({norm}_{\mathrm{op}}\left({T}\right)\le {A}↔sup\left(\left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)\le {A}\right)$
4 nmopsetretALT ${⊢}{T}:ℋ⟶ℋ\to \left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\}\subseteq ℝ$
5 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
6 4 5 sstrdi ${⊢}{T}:ℋ⟶ℋ\to \left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\}\subseteq {ℝ}^{*}$
7 supxrleub ${⊢}\left(\left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\}\subseteq {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left(sup\left(\left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)\le {A}↔\forall {z}\in \left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}\right)$
8 6 7 sylan ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in {ℝ}^{*}\right)\to \left(sup\left(\left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)\le {A}↔\forall {z}\in \left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}\right)$
9 ancom ${⊢}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)↔\left({y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)$
10 eqeq1 ${⊢}{y}={z}\to \left({y}={norm}_{ℎ}\left({T}\left({x}\right)\right)↔{z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)$
11 10 anbi1d ${⊢}{y}={z}\to \left(\left({y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)↔\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)$
12 9 11 syl5bb ${⊢}{y}={z}\to \left(\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)↔\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)$
13 12 rexbidv ${⊢}{y}={z}\to \left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)↔\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\right)$
14 13 ralab ${⊢}\forall {z}\in \left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)$
15 ralcom4 ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)$
16 impexp ${⊢}\left(\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)↔\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\to \left({norm}_{ℎ}\left({x}\right)\le 1\to {z}\le {A}\right)\right)$
17 16 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\to \left({norm}_{ℎ}\left({x}\right)\le 1\to {z}\le {A}\right)\right)$
18 fvex ${⊢}{norm}_{ℎ}\left({T}\left({x}\right)\right)\in \mathrm{V}$
19 breq1 ${⊢}{z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\to \left({z}\le {A}↔{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
20 19 imbi2d ${⊢}{z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\to \left(\left({norm}_{ℎ}\left({x}\right)\le 1\to {z}\le {A}\right)↔\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)\right)$
21 18 20 ceqsalv ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\to \left({norm}_{ℎ}\left({x}\right)\le 1\to {z}\le {A}\right)\right)↔\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
22 17 21 bitri ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)↔\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
23 22 ralbii ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
24 r19.23v ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)↔\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)$
25 24 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)$
26 15 23 25 3bitr3i ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({z}={norm}_{ℎ}\left({T}\left({x}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {z}\le {A}\right)$
27 14 26 bitr4i ${⊢}\forall {z}\in \left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
28 8 27 syl6bb ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in {ℝ}^{*}\right)\to \left(sup\left(\left\{{y}|\exists {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\wedge {y}={norm}_{ℎ}\left({T}\left({x}\right)\right)\right)\right\},{ℝ}^{*},<\right)\le {A}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)\right)$
29 3 28 bitrd ${⊢}\left({T}:ℋ⟶ℋ\wedge {A}\in {ℝ}^{*}\right)\to \left({norm}_{\mathrm{op}}\left({T}\right)\le {A}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)\right)$