# Metamath Proof Explorer

## Theorem nmopub2tALT

Description: An upper bound for an operator norm. (Contributed by NM, 12-Apr-2006) (New usage is discouraged.) (Proof modification is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 normcl ${⊢}{x}\in ℋ\to {norm}_{ℎ}\left({x}\right)\in ℝ$
2 1 ad2antlr ${⊢}\left(\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({x}\right)\in ℝ$
3 simpllr ${⊢}\left(\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left({A}\in ℝ\wedge 0\le {A}\right)$
4 simpr ${⊢}\left(\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {norm}_{ℎ}\left({x}\right)\le 1$
5 1re ${⊢}1\in ℝ$
6 lemul2a ${⊢}\left(\left({norm}_{ℎ}\left({x}\right)\in ℝ\wedge 1\in ℝ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {A}{norm}_{ℎ}\left({x}\right)\le {A}\cdot 1$
7 5 6 mp3anl2 ${⊢}\left(\left({norm}_{ℎ}\left({x}\right)\in ℝ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {A}{norm}_{ℎ}\left({x}\right)\le {A}\cdot 1$
8 2 3 4 7 syl21anc ${⊢}\left(\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {A}{norm}_{ℎ}\left({x}\right)\le {A}\cdot 1$
9 ax-1rid ${⊢}{A}\in ℝ\to {A}\cdot 1={A}$
10 9 ad2antrl ${⊢}\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\to {A}\cdot 1={A}$
11 10 ad2antrr ${⊢}\left(\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {A}\cdot 1={A}$
12 8 11 breqtrd ${⊢}\left(\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to {A}{norm}_{ℎ}\left({x}\right)\le {A}$
13 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
14 normcl ${⊢}{T}\left({x}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
15 13 14 syl ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
16 15 adantlr ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ$
17 remulcl ${⊢}\left({A}\in ℝ\wedge {norm}_{ℎ}\left({x}\right)\in ℝ\right)\to {A}{norm}_{ℎ}\left({x}\right)\in ℝ$
18 1 17 sylan2 ${⊢}\left({A}\in ℝ\wedge {x}\in ℋ\right)\to {A}{norm}_{ℎ}\left({x}\right)\in ℝ$
19 18 adantlr ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {x}\in ℋ\right)\to {A}{norm}_{ℎ}\left({x}\right)\in ℝ$
20 19 adantll ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\to {A}{norm}_{ℎ}\left({x}\right)\in ℝ$
21 simplrl ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\to {A}\in ℝ$
22 letr ${⊢}\left({norm}_{ℎ}\left({T}\left({x}\right)\right)\in ℝ\wedge {A}{norm}_{ℎ}\left({x}\right)\in ℝ\wedge {A}\in ℝ\right)\to \left(\left({norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\wedge {A}{norm}_{ℎ}\left({x}\right)\le {A}\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
23 16 20 21 22 syl3anc ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\to \left(\left({norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\wedge {A}{norm}_{ℎ}\left({x}\right)\le {A}\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
24 23 adantr ${⊢}\left(\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left(\left({norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\wedge {A}{norm}_{ℎ}\left({x}\right)\le {A}\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
25 12 24 mpan2d ${⊢}\left(\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\wedge {norm}_{ℎ}\left({x}\right)\le 1\right)\to \left({norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)$
26 25 ex ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\to \left({norm}_{ℎ}\left({x}\right)\le 1\to \left({norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)\right)$
27 26 com23 ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {x}\in ℋ\right)\to \left({norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\to \left({norm}_{ℎ}\left({x}\right)\le 1\to {norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}\right)\right)$
28 27 ralimdva ${⊢}\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\to \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 28 imp ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\right)\to \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)$
30 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
31 30 adantr ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to {A}\in {ℝ}^{*}$
32 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)$
33 31 32 sylan2 ${⊢}\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\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)$
34 33 biimpar ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge \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)\to {norm}_{\mathrm{op}}\left({T}\right)\le {A}$
35 29 34 syldan ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\right)\to {norm}_{\mathrm{op}}\left({T}\right)\le {A}$
36 35 3impa ${⊢}\left({T}:ℋ⟶ℋ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)\le {A}{norm}_{ℎ}\left({x}\right)\right)\to {norm}_{\mathrm{op}}\left({T}\right)\le {A}$