Theorem nmlnopgt0i

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
Hypothesis	nmlnop0.1	$$⊢T\in \mathrm{LinOp}$$
Assertion	nmlnopgt0i	$$⊢T\ne 0_{\mathrm{hop}}\leftrightarrow 0<{norm}_{\mathrm{op}}\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmlnop0.1	$$⊢T\in \mathrm{LinOp}$$
2	1	nmlnop0iHIL	$$⊢{norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow T=0_{\mathrm{hop}}$$
3	2	necon3bii	$$⊢{norm}_{\mathrm{op}}\left(T\right)\ne 0\leftrightarrow T\ne 0_{\mathrm{hop}}$$
4	1	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
5		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)$$
6	4 5	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(T\right)\ne 0\leftrightarrow 0<{norm}_{\mathrm{op}}\left(T\right)$$
7	3 6	bitr3i	$$⊢T\ne 0_{\mathrm{hop}}\leftrightarrow 0<{norm}_{\mathrm{op}}\left(T\right)$$