Metamath Proof Explorer


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 syl6bb ( 𝑇 : ℋ ⟶ ℋ → ( ( 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𝑇 ) )