Theorem nmopsetretHIL

Description: The set in the supremum of the operator norm definition df-nmop is a set of reals. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopsetretHIL	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(T\left(y\right)\right)\right)\right\}\subseteq ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2	1	hhnv	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$$
3		df-hba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
4	1	hhnm	$$⊢{norm}_{ℎ}={norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
5	3 4	nmosetre	$$⊢\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(T\left(y\right)\right)\right)\right\}\subseteq ℝ$$
6	2 5	mpan	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(T\left(y\right)\right)\right)\right\}\subseteq ℝ$$