Metamath Proof Explorer

Theorem nmoxr

Description: The norm of an operator is an extended real. (Contributed by NM, 27-Nov-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 nmoxr ⊢ 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 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
5 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
6 1 2 4 5 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 ℝ * <
7 2 5 nmosetre ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ⊆ ℝ
8 ressxr ⊢ ℝ ⊆ ℝ *
9 7 8 sstrdi ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ⊆ ℝ *
10 supxrcl ⊢ 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 9 10 syl ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ∈ ℝ *
12 11 3adant1 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → sup x | ∃ z ∈ X norm CV ⁡ U ⁡ z ≤ 1 ∧ x = norm CV ⁡ W ⁡ T ⁡ z ℝ * < ∈ ℝ *
13 6 12 eqeltrd ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ *