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 0hopContOp

Proof

Step Hyp Ref Expression
1 ho0f 0hop:
2 1rp 1+
3 ho0val w0hopw=0
4 ho0val x0hopx=0
5 3 4 oveqan12rd xw0hopw-0hopx=0-0
6 5 adantlr xy+w0hopw-0hopx=0-0
7 ax-hv0cl 0
8 hvsubid 00-0=0
9 7 8 ax-mp 0-0=0
10 6 9 eqtrdi xy+w0hopw-0hopx=0
11 10 fveq2d xy+wnorm0hopw-0hopx=norm0
12 norm0 norm0=0
13 11 12 eqtrdi xy+wnorm0hopw-0hopx=0
14 rpgt0 y+0<y
15 14 ad2antlr xy+w0<y
16 13 15 eqbrtrd xy+wnorm0hopw-0hopx<y
17 16 a1d xy+wnormw-x<1norm0hopw-0hopx<y
18 17 ralrimiva xy+wnormw-x<1norm0hopw-0hopx<y
19 breq2 z=1normw-x<znormw-x<1
20 19 rspceaimv 1+wnormw-x<1norm0hopw-0hopx<yz+wnormw-x<znorm0hopw-0hopx<y
21 2 18 20 sylancr xy+z+wnormw-x<znorm0hopw-0hopx<y
22 21 rgen2 xy+z+wnormw-x<znorm0hopw-0hopx<y
23 elcnop 0hopContOp0hop:xy+z+wnormw-x<znorm0hopw-0hopx<y
24 1 22 23 mpbir2an 0hopContOp