# 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}_{\mathrm{hop}}\in \mathrm{ContOp}$

### Proof

Step Hyp Ref Expression
1 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
2 1rp ${⊢}1\in {ℝ}^{+}$
3 ho0val ${⊢}{w}\in ℋ\to {0}_{\mathrm{hop}}\left({w}\right)={0}_{ℎ}$
4 ho0val ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
5 3 4 oveqan12rd ${⊢}\left({x}\in ℋ\wedge {w}\in ℋ\right)\to {0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}{-}_{ℎ}{0}_{ℎ}$
6 5 adantlr ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to {0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}{-}_{ℎ}{0}_{ℎ}$
7 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
8 hvsubid ${⊢}{0}_{ℎ}\in ℋ\to {0}_{ℎ}{-}_{ℎ}{0}_{ℎ}={0}_{ℎ}$
9 7 8 ax-mp ${⊢}{0}_{ℎ}{-}_{ℎ}{0}_{ℎ}={0}_{ℎ}$
10 6 9 syl6eq ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to {0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
11 10 fveq2d ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)={norm}_{ℎ}\left({0}_{ℎ}\right)$
12 norm0 ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)=0$
13 11 12 syl6eq ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)=0$
14 rpgt0 ${⊢}{y}\in {ℝ}^{+}\to 0<{y}$
15 14 ad2antlr ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to 0<{y}$
16 13 15 eqbrtrd ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)<{y}$
17 16 a1d ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to \left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<1\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)<{y}\right)$
18 17 ralrimiva ${⊢}\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\to \forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<1\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)<{y}\right)$
19 breq2 ${⊢}{z}=1\to \left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}↔{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<1\right)$
20 19 rspceaimv ${⊢}\left(1\in {ℝ}^{+}\wedge \forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<1\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)<{y}\right)\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)<{y}\right)$
21 2 18 20 sylancr ${⊢}\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)<{y}\right)$
22 21 rgen2 ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)<{y}\right)$
23 elcnop ${⊢}{0}_{\mathrm{hop}}\in \mathrm{ContOp}↔\left({0}_{\mathrm{hop}}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to {norm}_{ℎ}\left({0}_{\mathrm{hop}}\left({w}\right){-}_{ℎ}{0}_{\mathrm{hop}}\left({x}\right)\right)<{y}\right)\right)$
24 1 22 23 mpbir2an ${⊢}{0}_{\mathrm{hop}}\in \mathrm{ContOp}$