Theorem nmopxr

Description: The norm of a Hilbert space operator is an extended real. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopxr	$$⊢T:\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		nmopval	$$⊢T:\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(T\right)=sup\left(\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\},{ℝ}^{*},<\right)$$
2		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 ℝ$$
3		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
4	2 3	sstrdi	$$⊢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 {ℝ}^{*}$$
5		supxrcl	$$⊢\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 {ℝ}^{*}\to sup\left(\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\},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
6	4 5	syl	$$⊢T:\mathscr{H}⟶\mathscr{H}\to sup\left(\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\},{ℝ}^{*},<\right)\in {ℝ}^{*}$$
7	1 6	eqeltrd	$$⊢T:\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}$$