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 ⊢ X = BaseSet ⁡ U
nmoxr.2 ⊢ Y = BaseSet ⁡ W
nmoxr.3 ⊢ N = U normOp OLD W
Assertion nmoreltpnf ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ N ⁡ T < +∞

Proof

Step Hyp Ref Expression
1 nmoxr.1 ⊢ X = BaseSet ⁡ U
2 nmoxr.2 ⊢ Y = BaseSet ⁡ W
3 nmoxr.3 ⊢ N = U normOp OLD W
4 1 2 3 nmorepnf ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ N ⁡ T ≠ +∞
5 1 2 3 nmoxr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ *
6 nltpnft ⊢ N ⁡ T ∈ ℝ * → N ⁡ T = +∞ ↔ ¬ N ⁡ T < +∞
7 5 6 syl ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T = +∞ ↔ ¬ N ⁡ T < +∞
8 7 necon2abid ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T < +∞ ↔ N ⁡ T ≠ +∞
9 4 8 bitr4d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ N ⁡ T < +∞