Metamath Proof Explorer


Theorem 0cnop

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 0 hop ContOp

Proof

Step Hyp Ref Expression
1 ho0f 0 hop :
2 1rp 1 +
3 ho0val w 0 hop w = 0
4 ho0val x 0 hop x = 0
5 3 4 oveqan12rd x w 0 hop w - 0 hop x = 0 - 0
6 5 adantlr x y + w 0 hop w - 0 hop x = 0 - 0
7 ax-hv0cl 0
8 hvsubid 0 0 - 0 = 0
9 7 8 ax-mp 0 - 0 = 0
10 6 9 syl6eq x y + w 0 hop w - 0 hop x = 0
11 10 fveq2d x y + w norm 0 hop w - 0 hop x = norm 0
12 norm0 norm 0 = 0
13 11 12 syl6eq x y + w norm 0 hop w - 0 hop x = 0
14 rpgt0 y + 0 < y
15 14 ad2antlr x y + w 0 < y
16 13 15 eqbrtrd x y + w norm 0 hop w - 0 hop x < y
17 16 a1d x y + w norm w - x < 1 norm 0 hop w - 0 hop x < y
18 17 ralrimiva x y + w norm w - x < 1 norm 0 hop w - 0 hop x < y
19 breq2 z = 1 norm w - x < z norm w - x < 1
20 19 rspceaimv 1 + w norm w - x < 1 norm 0 hop w - 0 hop x < y z + w norm w - x < z norm 0 hop w - 0 hop x < y
21 2 18 20 sylancr x y + z + w norm w - x < z norm 0 hop w - 0 hop x < y
22 21 rgen2 x y + z + w norm w - x < z norm 0 hop w - 0 hop x < y
23 elcnop 0 hop ContOp 0 hop : x y + z + w norm w - x < z norm 0 hop w - 0 hop x < y
24 1 22 23 mpbir2an 0 hop ContOp