Metamath Proof Explorer

Theorem nmooval

Description: The operator norm function. (Contributed by NM, 27-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmoofval.1 ⊢ X = BaseSet ⁡ U
nmoofval.2 ⊢ Y = BaseSet ⁡ W
nmoofval.3 ⊢ L = norm CV ⁡ U
nmoofval.4 ⊢ M = norm CV ⁡ W
nmoofval.6 ⊢ N = U normOp OLD W
Assertion nmooval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T = sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z ℝ * <

Proof

Step Hyp Ref Expression
1 nmoofval.1 ⊢ X = BaseSet ⁡ U
2 nmoofval.2 ⊢ Y = BaseSet ⁡ W
3 nmoofval.3 ⊢ L = norm CV ⁡ U
4 nmoofval.4 ⊢ M = norm CV ⁡ W
5 nmoofval.6 ⊢ N = U normOp OLD W
6 2 fvexi ⊢ Y ∈ V
7 1 fvexi ⊢ X ∈ V
8 6 7 elmap ⊢ T ∈ Y X ↔ T : X ⟶ Y
9 1 2 3 4 5 nmoofval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → N = t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * <
10 9 fveq1d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → N ⁡ T = t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * < ⁡ T
11 fveq1 ⊢ t = T → t ⁡ z = T ⁡ z
12 11 fveq2d ⊢ t = T → M ⁡ t ⁡ z = M ⁡ T ⁡ z
13 12 eqeq2d ⊢ t = T → x = M ⁡ t ⁡ z ↔ x = M ⁡ T ⁡ z
14 13 anbi2d ⊢ t = T → L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ↔ L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z
15 14 rexbidv ⊢ t = T → ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ↔ ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z
16 15 abbidv ⊢ t = T → x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z = x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z
17 16 supeq1d ⊢ t = T → sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * < = sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z ℝ * <
18 eqid ⊢ t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * < = t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * <
19 xrltso ⊢ < Or ℝ *
20 19 supex ⊢ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z ℝ * < ∈ V
21 17 18 20 fvmpt ⊢ T ∈ Y X → t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * < ⁡ T = sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z ℝ * <
22 10 21 sylan9eq ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ Y X → N ⁡ T = sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z ℝ * <
23 8 22 sylan2br ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T = sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z ℝ * <
24 23 3impa ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T = sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ T ⁡ z ℝ * <