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 ⊢ X = BaseSet ⁡ U
nmoxr.2 ⊢ Y = BaseSet ⁡ W
nmoxr.3 ⊢ N = U normOp OLD W
Assertion nmogtmnf ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → −∞ < 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 df-ne ⊢ N ⁡ T ≠ +∞ ↔ ¬ N ⁡ T = +∞
6 4 5 bitrdi ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ ¬ N ⁡ T = +∞
7 xor3 ⊢ ¬ N ⁡ T ∈ ℝ ↔ N ⁡ T = +∞ ↔ N ⁡ T ∈ ℝ ↔ ¬ N ⁡ T = +∞
8 nbior ⊢ ¬ N ⁡ T ∈ ℝ ↔ N ⁡ T = +∞ → N ⁡ T ∈ ℝ ∨ N ⁡ T = +∞
9 7 8 sylbir ⊢ N ⁡ T ∈ ℝ ↔ ¬ N ⁡ T = +∞ → N ⁡ T ∈ ℝ ∨ N ⁡ T = +∞
10 mnfltxr ⊢ N ⁡ T ∈ ℝ ∨ N ⁡ T = +∞ → −∞ < N ⁡ T
11 6 9 10 3syl ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → −∞ < N ⁡ T