Theorem nmopgt0

Description: A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopgt0	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)\ne 0\leftrightarrow 0<{norm}_{\mathrm{op}}\left(T\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmopxr	$$⊢T:\mathscr{H}⟶\mathscr{H}\to {norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}$$
2		nmopge0	$$⊢T:\mathscr{H}⟶\mathscr{H}\to 0\le {norm}_{\mathrm{op}}\left(T\right)$$
3		0xr	$$⊢0\in {ℝ}^{*}$$
4		xrleltne	$$⊢\left(0\in {ℝ}^{*}\wedge {norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}\wedge 0\le {norm}_{\mathrm{op}}\left(T\right)\right)\to \left(0<{norm}_{\mathrm{op}}\left(T\right)\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)\ne 0\right)$$
5	3 4	mp3an1	$$⊢\left({norm}_{\mathrm{op}}\left(T\right)\in {ℝ}^{*}\wedge 0\le {norm}_{\mathrm{op}}\left(T\right)\right)\to \left(0<{norm}_{\mathrm{op}}\left(T\right)\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)\ne 0\right)$$
6	1 2 5	syl2anc	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left(0<{norm}_{\mathrm{op}}\left(T\right)\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)\ne 0\right)$$
7	6	bicomd	$$⊢T:\mathscr{H}⟶\mathscr{H}\to \left({norm}_{\mathrm{op}}\left(T\right)\ne 0\leftrightarrow 0<{norm}_{\mathrm{op}}\left(T\right)\right)$$