This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 LinOp$
	Assertion	nmlnopgt0i	$⊢ T \neq 0_{hop} \leftrightarrow 0 < {norm}_{op} (T)$

Proof

Step	Hyp	Ref	Expression
1		nmlnop0.1	$⊢ T \in LinOp$
2	1	nmlnop0iHIL	$⊢ {norm}_{op} (T) = 0 \leftrightarrow T = 0_{hop}$
3	2	necon3bii	$⊢ {norm}_{op} (T) \neq 0 \leftrightarrow T \neq 0_{hop}$
4	1	lnopfi	$⊢ T : ℋ ⟶ ℋ$
5		nmopgt0	$⊢ T : ℋ ⟶ ℋ \to ({norm}_{op} (T) \neq 0 \leftrightarrow 0 < {norm}_{op} (T))$
6	4 5	ax-mp	$⊢ {norm}_{op} (T) \neq 0 \leftrightarrow 0 < {norm}_{op} (T)$
7	3 6	bitr3i	$⊢ T \neq 0_{hop} \leftrightarrow 0 < {norm}_{op} (T)$