Metamath Proof Explorer

Theorem nmoofval

Description: The operator norm function. (Contributed by NM, 6-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 nmoofval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → N = t ∈ Y X ⟼ 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 fveq2 ⊢ u = U → BaseSet ⁡ u = BaseSet ⁡ U
7 6 1 eqtr4di ⊢ u = U → BaseSet ⁡ u = X
8 7 oveq2d ⊢ u = U → BaseSet ⁡ w BaseSet ⁡ u = BaseSet ⁡ w X
9 fveq2 ⊢ u = U → norm CV ⁡ u = norm CV ⁡ U
10 9 3 eqtr4di ⊢ u = U → norm CV ⁡ u = L
11 10 fveq1d ⊢ u = U → norm CV ⁡ u ⁡ z = L ⁡ z
12 11 breq1d ⊢ u = U → norm CV ⁡ u ⁡ z ≤ 1 ↔ L ⁡ z ≤ 1
13 12 anbi1d ⊢ u = U → norm CV ⁡ u ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ↔ L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z
14 7 13 rexeqbidv ⊢ u = U → ∃ z ∈ BaseSet ⁡ u norm CV ⁡ u ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ↔ ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z
15 14 abbidv ⊢ u = U → x | ∃ z ∈ BaseSet ⁡ u norm CV ⁡ u ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z = x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z
16 15 supeq1d ⊢ u = U → sup x | ∃ z ∈ BaseSet ⁡ u norm CV ⁡ u ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ℝ * < = sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ℝ * <
17 8 16 mpteq12dv ⊢ u = U → t ∈ BaseSet ⁡ w BaseSet ⁡ u ⟼ sup x | ∃ z ∈ BaseSet ⁡ u norm CV ⁡ u ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ℝ * < = t ∈ BaseSet ⁡ w X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ℝ * <
18 fveq2 ⊢ w = W → BaseSet ⁡ w = BaseSet ⁡ W
19 18 2 eqtr4di ⊢ w = W → BaseSet ⁡ w = Y
20 19 oveq1d ⊢ w = W → BaseSet ⁡ w X = Y X
21 fveq2 ⊢ w = W → norm CV ⁡ w = norm CV ⁡ W
22 21 4 eqtr4di ⊢ w = W → norm CV ⁡ w = M
23 22 fveq1d ⊢ w = W → norm CV ⁡ w ⁡ t ⁡ z = M ⁡ t ⁡ z
24 23 eqeq2d ⊢ w = W → x = norm CV ⁡ w ⁡ t ⁡ z ↔ x = M ⁡ t ⁡ z
25 24 anbi2d ⊢ w = W → L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ↔ L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z
26 25 rexbidv ⊢ w = W → ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ↔ ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z
27 26 abbidv ⊢ w = W → x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z = x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z
28 27 supeq1d ⊢ w = W → sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ℝ * < = sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * <
29 20 28 mpteq12dv ⊢ w = W → t ∈ BaseSet ⁡ w X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ℝ * < = t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * <
30 df-nmoo ⊢ normOp OLD = u ∈ NrmCVec , w ∈ NrmCVec ⟼ t ∈ BaseSet ⁡ w BaseSet ⁡ u ⟼ sup x | ∃ z ∈ BaseSet ⁡ u norm CV ⁡ u ⁡ z ≤ 1 ∧ x = norm CV ⁡ w ⁡ t ⁡ z ℝ * <
31 ovex ⊢ Y X ∈ V
32 31 mptex ⊢ t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * < ∈ V
33 17 29 30 32 ovmpo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → U normOp OLD W = t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * <
34 5 33 eqtrid ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → N = t ∈ Y X ⟼ sup x | ∃ z ∈ X L ⁡ z ≤ 1 ∧ x = M ⁡ t ⁡ z ℝ * <