Theorem nmopre

Description: The norm of a bounded operator is a real number. (Contributed by NM, 29-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopre	$$⊢T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		bdopf	$$⊢T\in \mathrm{BndLinOp}\to T:\mathscr{H}⟶\mathscr{H}$$
2		nmopgtmnf	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left(T\right)$$
3	1 2	syl	$$⊢T\in \mathrm{BndLinOp}\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left(T\right)$$
4		elbdop	$$⊢T\in \mathrm{BndLinOp}\leftrightarrow \left(T\in \mathrm{LinOp}\wedge {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)$$
5	4	simprbi	$$⊢T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }$$
6		nmopxr	$$⊢T:\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}$$
7		xrrebnd	$$⊢{norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow \left(\mathrm{-\infty }<{norm}_{\mathrm{op}}\left(T\right)\wedge {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)\right)$$
8	1 6 7	3syl	$$⊢T\in \mathrm{BndLinOp}\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow \left(\mathrm{-\infty }<{norm}_{\mathrm{op}}\left(T\right)\wedge {norm}_{\mathrm{op}}\left(T\right)<\mathrm{+\infty }\right)\right)$$
9	3 5 8	mpbir2and	$$⊢T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$