# Metamath Proof Explorer

## Theorem nmopub2tHIL

Description: An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007) (New usage is discouraged.)

Ref Expression
Assertion nmopub2tHIL ${⊢}\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 df-hba ${⊢}ℋ=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
2 eqid ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
3 2 hhnm ${⊢}{norm}_{ℎ}={norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
4 eqid ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩{normOp}_{\mathrm{OLD}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩{normOp}_{\mathrm{OLD}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
5 2 4 hhnmoi ${⊢}{norm}_{\mathrm{op}}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩{normOp}_{\mathrm{OLD}}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
6 2 hhnv ${⊢}⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$
7 1 1 3 3 5 6 6 nmoub2i ${⊢}\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}$