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

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 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 ‘ 𝑇 ) )