Metamath Proof Explorer


Theorem nmopval

Description: Value of the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion nmopval T : norm op T = sup x | y norm y 1 x = norm T y * <

Proof

Step Hyp Ref Expression
1 xrltso < Or *
2 1 supex sup x | y norm y 1 x = norm T y * < V
3 ax-hilex V
4 fveq1 t = T t y = T y
5 4 fveq2d t = T norm t y = norm T y
6 5 eqeq2d t = T x = norm t y x = norm T y
7 6 anbi2d t = T norm y 1 x = norm t y norm y 1 x = norm T y
8 7 rexbidv t = T y norm y 1 x = norm t y y norm y 1 x = norm T y
9 8 abbidv t = T x | y norm y 1 x = norm t y = x | y norm y 1 x = norm T y
10 9 supeq1d t = T sup x | y norm y 1 x = norm t y * < = sup x | y norm y 1 x = norm T y * <
11 df-nmop norm op = t sup x | y norm y 1 x = norm t y * <
12 2 3 3 10 11 fvmptmap T : norm op T = sup x | y norm y 1 x = norm T y * <