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

Metamath Proof Explorer

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