Theorem nmopgtmnf

Description: The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmopgtmnf	⊢ ( 𝑇 : ℋ ⟶ ℋ → -∞ < ( normop ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		nmoprepnf	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ 𝑇 ) ≠ +∞ ) )
2		df-ne	⊢ ( ( normop ‘ 𝑇 ) ≠ +∞ ↔ ¬ ( normop ‘ 𝑇 ) = +∞ )
3	1 2	bitrdi	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ¬ ( normop ‘ 𝑇 ) = +∞ ) )
4		xor3	⊢ ( ¬ ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ 𝑇 ) = +∞ ) ↔ ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ¬ ( normop ‘ 𝑇 ) = +∞ ) )
5		nbior	⊢ ( ¬ ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ( normop ‘ 𝑇 ) = +∞ ) → ( ( normop ‘ 𝑇 ) ∈ ℝ ∨ ( normop ‘ 𝑇 ) = +∞ ) )
6	4 5	sylbir	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ↔ ¬ ( normop ‘ 𝑇 ) = +∞ ) → ( ( normop ‘ 𝑇 ) ∈ ℝ ∨ ( normop ‘ 𝑇 ) = +∞ ) )
7		mnfltxr	⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∨ ( normop ‘ 𝑇 ) = +∞ ) → -∞ < ( normop ‘ 𝑇 ) )
8	3 6 7	3syl	⊢ ( 𝑇 : ℋ ⟶ ℋ → -∞ < ( normop ‘ 𝑇 ) )