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:\mathscr{H}⟶\mathscr{H}\wedge \left(A\in ℝ\wedge 0\le A\right)\wedge \forall x\in \mathscr{H}{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	$$⊢\mathscr{H}=\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:\mathscr{H}⟶\mathscr{H}\wedge \left(A\in ℝ\wedge 0\le A\right)\wedge \forall x\in \mathscr{H}{norm}_{ℎ}\left(T\left(x\right)\right)\le A{norm}_{ℎ}\left(x\right)\right)\to {norm}_{\mathrm{op}}\left(T\right)\le A$$