Metamath Proof Explorer

Theorem nmorepnf

Description: The norm of an operator is either real or 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 nmorepnf ⊢ 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 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
5 2 4 nmosetre ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ⊆ ℝ
6 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
7 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
8 1 6 7 nmosetn0 ⊢ U ∈ NrmCVec → norm CV ⁡ W ⁡ T ⁡ 0 vec ⁡ U ∈ x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z
9 8 ne0d ⊢ U ∈ NrmCVec → x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ≠ ∅
10 supxrre2 ⊢ x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ⊆ ℝ ∧ x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ≠ ∅ → sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ∈ ℝ ↔ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ≠ +∞
11 5 9 10 syl2anr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ∈ ℝ ↔ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ≠ +∞
12 11 3impb ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ∈ ℝ ↔ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ≠ +∞
13 1 2 7 4 3 nmooval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T = sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * <
14 13 eleq1d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ∈ ℝ
15 13 neeq1d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ≠ +∞ ↔ sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ≠ +∞
16 12 14 15 3bitr4d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ N ⁡ T ≠ +∞