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