Theorem nmopgtmnf

Description: The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopgtmnf	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmoprepnf	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)\ne \mathrm{+\infty }\right)$$
2		df-ne	$$⊢{norm}_{\mathrm{op}}\left(T\right)\ne \mathrm{+\infty }\leftrightarrow \neg {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }$$
3	1 2	bitrdi	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow \neg {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\right)$$
4		xor3	$$⊢\neg \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\right)\leftrightarrow \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow \neg {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\right)$$
5		nbior	$$⊢\neg \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\right)\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\vee {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\right)$$
6	4 5	sylbir	$$⊢\left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\leftrightarrow \neg {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\right)\to \left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\vee {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\right)$$
7		mnfltxr	$$⊢\left({norm}_{\mathrm{op}}\left(T\right)\in ℝ\vee {norm}_{\mathrm{op}}\left(T\right)=\mathrm{+\infty }\right)\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left(T\right)$$
8	3 6 7	3syl	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left(T\right)$$