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 ∧ 𝑇 : 𝑋𝑌 ) → -∞ < ( 𝑁𝑇 ) )