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	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ 𝑇 ) < +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		nmoprepnf	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ 𝑇 ) ≠ +∞ ) )
2		nmopxr	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) ∈ ℝ* )
3		nltpnft	⊢ ( ( normop ‘ 𝑇 ) ∈ ℝ* → ( ( normop ‘ 𝑇 ) = +∞ ↔ ¬ ( normop ‘ 𝑇 ) < +∞ ) )
4	2 3	syl	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) = +∞ ↔ ¬ ( normop ‘ 𝑇 ) < +∞ ) )
5	4	necon2abid	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) < +∞ ↔ ( normop ‘ 𝑇 ) ≠ +∞ ) )
6	1 5	bitr4d	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ 𝑇 ) < +∞ ) )