Metamath Proof Explorer

Theorem nmblore

Description: The norm of a bounded operator is a real number. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmblore.1 ⊢ X = BaseSet ⁡ U
nmblore.2 ⊢ Y = BaseSet ⁡ W
nmblore.3 ⊢ N = U normOp OLD W
nmblore.5 ⊢ B = U BLnOp W
Assertion nmblore ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → N ⁡ T ∈ ℝ

Proof

Step Hyp Ref Expression
1 nmblore.1 ⊢ X = BaseSet ⁡ U
2 nmblore.2 ⊢ Y = BaseSet ⁡ W
3 nmblore.3 ⊢ N = U normOp OLD W
4 nmblore.5 ⊢ B = U BLnOp W
5 1 2 4 blof ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → T : X ⟶ Y
6 1 2 3 nmogtmnf ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → −∞ < N ⁡ T
7 5 6 syld3an3 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → −∞ < N ⁡ T
8 eqid ⊢ U LnOp W = U LnOp W
9 3 8 4 isblo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → T ∈ B ↔ T ∈ U LnOp W ∧ N ⁡ T < +∞
10 9 simplbda ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → N ⁡ T < +∞
11 10 3impa ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → N ⁡ T < +∞
12 1 2 3 nmoxr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ *
13 5 12 syld3an3 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → N ⁡ T ∈ ℝ *
14 xrrebnd ⊢ N ⁡ T ∈ ℝ * → N ⁡ T ∈ ℝ ↔ −∞ < N ⁡ T ∧ N ⁡ T < +∞
15 13 14 syl ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → N ⁡ T ∈ ℝ ↔ −∞ < N ⁡ T ∧ N ⁡ T < +∞
16 7 11 15 mpbir2and ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ B → N ⁡ T ∈ ℝ