Theorem nmopsetretALT

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.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	nmopsetretALT	$$⊢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		ffvelcdm	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge y\in \mathscr{H}\right)\to T\left(y\right)\in \mathscr{H}$$
2		normcl	$$⊢T\left(y\right)\in \mathscr{H}\to {norm}_{ℎ}\left(T\left(y\right)\right)\in ℝ$$
3	1 2	syl	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge y\in \mathscr{H}\right)\to {norm}_{ℎ}\left(T\left(y\right)\right)\in ℝ$$
4		eleq1	$$⊢x={norm}_{ℎ}\left(T\left(y\right)\right)\to \left(x\in ℝ\leftrightarrow {norm}_{ℎ}\left(T\left(y\right)\right)\in ℝ\right)$$
5	3 4	imbitrrid	$$⊢x={norm}_{ℎ}\left(T\left(y\right)\right)\to \left(\left(T:\mathscr{H}⟶\mathscr{H}\wedge y\in \mathscr{H}\right)\to x\in ℝ\right)$$
6	5	impcom	$$⊢\left(\left(T:\mathscr{H}⟶\mathscr{H}\wedge y\in \mathscr{H}\right)\wedge x={norm}_{ℎ}\left(T\left(y\right)\right)\right)\to x\in ℝ$$
7	6	adantrl	$$⊢\left(\left(T:\mathscr{H}⟶\mathscr{H}\wedge y\in \mathscr{H}\right)\wedge \left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(T\left(y\right)\right)\right)\right)\to x\in ℝ$$
8	7	exp31	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(y\in \mathscr{H}\to \left(\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(T\left(y\right)\right)\right)\to x\in ℝ\right)\right)$$
9	8	rexlimdv	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(T\left(y\right)\right)\right)\to x\in ℝ\right)$$
10	9	abssdv	$$⊢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 ℝ$$