Description: The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 0cnop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ho0f | |
|
2 | 1rp | |
|
3 | ho0val | |
|
4 | ho0val | |
|
5 | 3 4 | oveqan12rd | |
6 | 5 | adantlr | |
7 | ax-hv0cl | |
|
8 | hvsubid | |
|
9 | 7 8 | ax-mp | |
10 | 6 9 | eqtrdi | |
11 | 10 | fveq2d | |
12 | norm0 | |
|
13 | 11 12 | eqtrdi | |
14 | rpgt0 | |
|
15 | 14 | ad2antlr | |
16 | 13 15 | eqbrtrd | |
17 | 16 | a1d | |
18 | 17 | ralrimiva | |
19 | breq2 | |
|
20 | 19 | rspceaimv | |
21 | 2 18 20 | sylancr | |
22 | 21 | rgen2 | |
23 | elcnop | |
|
24 | 1 22 23 | mpbir2an | |