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}}:\mathscr{H}⟶\mathscr{H}$$
2		1rp	$$⊢1\in {ℝ}^{+}$$
3		ho0val	$$⊢w\in \mathscr{H}\to 0_{\mathrm{hop}}\left(w\right)=0_{ℎ}$$
4		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
5	3 4	oveqan12rd	$$⊢\left(x\in \mathscr{H}\wedge w\in \mathscr{H}\right)\to 0_{\mathrm{hop}}\left(w\right){-}_{ℎ}{0}_{\mathrm{hop}}\left(x\right)=0_{ℎ}{-}_{ℎ}{0}_{ℎ}$$
6	5	adantlr	$$⊢\left(\left(x\in \mathscr{H}\wedge y\in {ℝ}^{+}\right)\wedge w\in \mathscr{H}\right)\to 0_{\mathrm{hop}}\left(w\right){-}_{ℎ}{0}_{\mathrm{hop}}\left(x\right)=0_{ℎ}{-}_{ℎ}{0}_{ℎ}$$
7		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
8		hvsubid	$$⊢0_{ℎ}\in \mathscr{H}\to 0_{ℎ}{-}_{ℎ}{0}_{ℎ}=0_{ℎ}$$
9	7 8	ax-mp	$$⊢0_{ℎ}{-}_{ℎ}{0}_{ℎ}=0_{ℎ}$$
10	6 9	eqtrdi	$$⊢\left(\left(x\in \mathscr{H}\wedge y\in {ℝ}^{+}\right)\wedge w\in \mathscr{H}\right)\to 0_{\mathrm{hop}}\left(w\right){-}_{ℎ}{0}_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
11	10	fveq2d	$$⊢\left(\left(x\in \mathscr{H}\wedge y\in {ℝ}^{+}\right)\wedge w\in \mathscr{H}\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	eqtrdi	$$⊢\left(\left(x\in \mathscr{H}\wedge y\in {ℝ}^{+}\right)\wedge w\in \mathscr{H}\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 \mathscr{H}\wedge y\in {ℝ}^{+}\right)\wedge w\in \mathscr{H}\right)\to 0<y$$
16	13 15	eqbrtrd	$$⊢\left(\left(x\in \mathscr{H}\wedge y\in {ℝ}^{+}\right)\wedge w\in \mathscr{H}\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 \mathscr{H}\wedge y\in {ℝ}^{+}\right)\wedge w\in \mathscr{H}\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 \mathscr{H}\wedge y\in {ℝ}^{+}\right)\to \forall w\in \mathscr{H}\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\leftrightarrow {norm}_{ℎ}\left(w{-}_{ℎ}x\right)<1\right)$$
20	19	rspceaimv	$$⊢\left(1\in {ℝ}^{+}\wedge \forall w\in \mathscr{H}\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 {ℝ}^{+}\forall w\in \mathscr{H}\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 \mathscr{H}\wedge y\in {ℝ}^{+}\right)\to \exists z\in {ℝ}^{+}\forall w\in \mathscr{H}\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 \mathscr{H}\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in \mathscr{H}\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}\leftrightarrow \left(0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in \mathscr{H}\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}$$