Metamath Proof Explorer


Theorem nmoo0

Description: The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoo0.3 N = U normOp OLD W
nmoo0.0 Z = U 0 op W
Assertion nmoo0 U NrmCVec W NrmCVec N Z = 0

Proof

Step Hyp Ref Expression
1 nmoo0.3 N = U normOp OLD W
2 nmoo0.0 Z = U 0 op W
3 eqid BaseSet U = BaseSet U
4 eqid BaseSet W = BaseSet W
5 3 4 2 0oo U NrmCVec W NrmCVec Z : BaseSet U BaseSet W
6 eqid norm CV U = norm CV U
7 eqid norm CV W = norm CV W
8 3 4 6 7 1 nmooval U NrmCVec W NrmCVec Z : BaseSet U BaseSet W N Z = sup x | z BaseSet U norm CV U z 1 x = norm CV W Z z * <
9 5 8 mpd3an3 U NrmCVec W NrmCVec N Z = sup x | z BaseSet U norm CV U z 1 x = norm CV W Z z * <
10 df-sn 0 = x | x = 0
11 eqid 0 vec U = 0 vec U
12 3 11 nvzcl U NrmCVec 0 vec U BaseSet U
13 11 6 nvz0 U NrmCVec norm CV U 0 vec U = 0
14 0le1 0 1
15 13 14 eqbrtrdi U NrmCVec norm CV U 0 vec U 1
16 fveq2 z = 0 vec U norm CV U z = norm CV U 0 vec U
17 16 breq1d z = 0 vec U norm CV U z 1 norm CV U 0 vec U 1
18 17 rspcev 0 vec U BaseSet U norm CV U 0 vec U 1 z BaseSet U norm CV U z 1
19 12 15 18 syl2anc U NrmCVec z BaseSet U norm CV U z 1
20 19 biantrurd U NrmCVec x = 0 z BaseSet U norm CV U z 1 x = 0
21 20 adantr U NrmCVec W NrmCVec x = 0 z BaseSet U norm CV U z 1 x = 0
22 eqid 0 vec W = 0 vec W
23 3 22 2 0oval U NrmCVec W NrmCVec z BaseSet U Z z = 0 vec W
24 23 3expa U NrmCVec W NrmCVec z BaseSet U Z z = 0 vec W
25 24 fveq2d U NrmCVec W NrmCVec z BaseSet U norm CV W Z z = norm CV W 0 vec W
26 22 7 nvz0 W NrmCVec norm CV W 0 vec W = 0
27 26 ad2antlr U NrmCVec W NrmCVec z BaseSet U norm CV W 0 vec W = 0
28 25 27 eqtrd U NrmCVec W NrmCVec z BaseSet U norm CV W Z z = 0
29 28 eqeq2d U NrmCVec W NrmCVec z BaseSet U x = norm CV W Z z x = 0
30 29 anbi2d U NrmCVec W NrmCVec z BaseSet U norm CV U z 1 x = norm CV W Z z norm CV U z 1 x = 0
31 30 rexbidva U NrmCVec W NrmCVec z BaseSet U norm CV U z 1 x = norm CV W Z z z BaseSet U norm CV U z 1 x = 0
32 r19.41v z BaseSet U norm CV U z 1 x = 0 z BaseSet U norm CV U z 1 x = 0
33 31 32 syl6rbb U NrmCVec W NrmCVec z BaseSet U norm CV U z 1 x = 0 z BaseSet U norm CV U z 1 x = norm CV W Z z
34 21 33 bitrd U NrmCVec W NrmCVec x = 0 z BaseSet U norm CV U z 1 x = norm CV W Z z
35 34 abbidv U NrmCVec W NrmCVec x | x = 0 = x | z BaseSet U norm CV U z 1 x = norm CV W Z z
36 10 35 syl5req U NrmCVec W NrmCVec x | z BaseSet U norm CV U z 1 x = norm CV W Z z = 0
37 36 supeq1d U NrmCVec W NrmCVec sup x | z BaseSet U norm CV U z 1 x = norm CV W Z z * < = sup 0 * <
38 9 37 eqtrd U NrmCVec W NrmCVec N Z = sup 0 * <
39 xrltso < Or *
40 0xr 0 *
41 supsn < Or * 0 * sup 0 * < = 0
42 39 40 41 mp2an sup 0 * < = 0
43 38 42 syl6eq U NrmCVec W NrmCVec N Z = 0