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 syl6eqr 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 syl6eqr 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 syl6eqr 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 syl6eqr 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 syl5eq U NrmCVec W NrmCVec N = t Y X sup x | z X L z 1 x = M t z * <