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

Metamath Proof Explorer

Theorem nmopreltpnf

Description: The norm of a Hilbert space operator is real iff it is less than infinity. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	nmopreltpnf	$⊢ T : ℋ ⟶ ℋ \to ({norm}_{op} (T) \in ℝ \leftrightarrow {norm}_{op} (T) < +∞)$

Proof

Step	Hyp	Ref	Expression
1		nmoprepnf	$⊢ T : ℋ ⟶ ℋ \to ({norm}_{op} (T) \in ℝ \leftrightarrow {norm}_{op} (T) \neq +∞)$
2		nmopxr	$⊢ T : ℋ ⟶ ℋ \to {norm}_{op} (T) \in ℝ^{*}$
3		nltpnft	$⊢ {norm}_{op} (T) \in ℝ^{*} \to ({norm}_{op} (T) = +∞ \leftrightarrow \neg {norm}_{op} (T) < +∞)$
4	2 3	syl	$⊢ T : ℋ ⟶ ℋ \to ({norm}_{op} (T) = +∞ \leftrightarrow \neg {norm}_{op} (T) < +∞)$
5	4	necon2abid	$⊢ T : ℋ ⟶ ℋ \to ({norm}_{op} (T) < +∞ \leftrightarrow {norm}_{op} (T) \neq +∞)$
6	1 5	bitr4d	$⊢ T : ℋ ⟶ ℋ \to ({norm}_{op} (T) \in ℝ \leftrightarrow {norm}_{op} (T) < +∞)$