Theorem nmoreltpnf

Description: The norm of any operator is real iff it is less than plus infinity. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoxr.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nmoxr.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	nmoxr.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
Assertion	nmoreltpnf	⊢ ( ( 𝑈 ∈ 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	1 2 3	nmoxr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ* )
6		nltpnft	⊢ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* → ( ( 𝑁 ‘ 𝑇 ) = +∞ ↔ ¬ ( 𝑁 ‘ 𝑇 ) < +∞ ) )
7	5 6	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) = +∞ ↔ ¬ ( 𝑁 ‘ 𝑇 ) < +∞ ) )
8	7	necon2abid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) < +∞ ↔ ( 𝑁 ‘ 𝑇 ) ≠ +∞ ) )
9	4 8	bitr4d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) < +∞ ) )