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

Metamath Proof Explorer

Theorem nmogtmnf

Description: The norm of an operator is greater than minus infinity. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoxr.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmoxr.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmoxr.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
Assertion nmogtmnf ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → -∞ < ( 𝑁 ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 nmoxr.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoxr.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoxr.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
4 1 2 3 nmorepnf ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) ≠ +∞ ) )
5 df-ne ⊢ ( ( 𝑁 ‘ 𝑇 ) ≠ +∞ ↔ ¬ ( 𝑁 ‘ 𝑇 ) = +∞ )
6 4 5 bitrdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ¬ ( 𝑁 ‘ 𝑇 ) = +∞ ) )
7 xor3 ⊢ ( ¬ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) = +∞ ) ↔ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ¬ ( 𝑁 ‘ 𝑇 ) = +∞ ) )
8 nbior ⊢ ( ¬ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) = +∞ ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ∨ ( 𝑁 ‘ 𝑇 ) = +∞ ) )
9 7 8 sylbir ⊢ ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ¬ ( 𝑁 ‘ 𝑇 ) = +∞ ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ∨ ( 𝑁 ‘ 𝑇 ) = +∞ ) )
10 mnfltxr ⊢ ( ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ∨ ( 𝑁 ‘ 𝑇 ) = +∞ ) → -∞ < ( 𝑁 ‘ 𝑇 ) )
11 6 9 10 3syl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → -∞ < ( 𝑁 ‘ 𝑇 ) )