Metamath Proof Explorer


Theorem nmop0

Description: The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmop0 norm op 0 hop = 0

Proof

Step Hyp Ref Expression
1 ho0f 0 hop :
2 nmopval 0 hop : norm op 0 hop = sup x | y norm y 1 x = norm 0 hop y * <
3 1 2 ax-mp norm op 0 hop = sup x | y norm y 1 x = norm 0 hop y * <
4 ho0val y 0 hop y = 0
5 4 fveq2d y norm 0 hop y = norm 0
6 norm0 norm 0 = 0
7 5 6 syl6eq y norm 0 hop y = 0
8 7 eqeq2d y x = norm 0 hop y x = 0
9 8 anbi2d y norm y 1 x = norm 0 hop y norm y 1 x = 0
10 9 rexbiia y norm y 1 x = norm 0 hop y y norm y 1 x = 0
11 ax-hv0cl 0
12 0le1 0 1
13 fveq2 y = 0 norm y = norm 0
14 13 6 syl6eq y = 0 norm y = 0
15 14 breq1d y = 0 norm y 1 0 1
16 15 rspcev 0 0 1 y norm y 1
17 11 12 16 mp2an y norm y 1
18 r19.41v y norm y 1 x = 0 y norm y 1 x = 0
19 17 18 mpbiran y norm y 1 x = 0 x = 0
20 10 19 bitri y norm y 1 x = norm 0 hop y x = 0
21 20 abbii x | y norm y 1 x = norm 0 hop y = x | x = 0
22 df-sn 0 = x | x = 0
23 21 22 eqtr4i x | y norm y 1 x = norm 0 hop y = 0
24 23 supeq1i sup x | y norm y 1 x = norm 0 hop y * < = sup 0 * <
25 xrltso < Or *
26 0xr 0 *
27 supsn < Or * 0 * sup 0 * < = 0
28 25 26 27 mp2an sup 0 * < = 0
29 3 24 28 3eqtri norm op 0 hop = 0