# Metamath Proof Explorer

## Theorem 0cnfn

Description: The identically zero function is a continuous Hilbert space functional. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion 0cnfn ${⊢}ℋ×\left\{0\right\}\in \mathrm{ContFn}$

### Proof

Step Hyp Ref Expression
1 0cn ${⊢}0\in ℂ$
2 1 fconst6 ${⊢}\left(ℋ×\left\{0\right\}\right):ℋ⟶ℂ$
3 1rp ${⊢}1\in {ℝ}^{+}$
4 c0ex ${⊢}0\in \mathrm{V}$
5 4 fvconst2 ${⊢}{w}\in ℋ\to \left(ℋ×\left\{0\right\}\right)\left({w}\right)=0$
6 4 fvconst2 ${⊢}{x}\in ℋ\to \left(ℋ×\left\{0\right\}\right)\left({x}\right)=0$
7 5 6 oveqan12rd ${⊢}\left({x}\in ℋ\wedge {w}\in ℋ\right)\to \left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\left({x}\right)=0-0$
8 7 adantlr ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to \left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\left({x}\right)=0-0$
9 0m0e0 ${⊢}0-0=0$
10 8 9 eqtrdi ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to \left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\left({x}\right)=0$
11 10 fveq2d ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\left({x}\right)\right|=\left|0\right|$
12 abs0 ${⊢}\left|0\right|=0$
13 11 12 eqtrdi ${⊢}\left(\left({x}\in ℋ\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in ℋ\right)\to \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\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 \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\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 \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\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 \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\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 \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\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 \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\left({x}\right)\right|<{y}\right)$
21 3 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 \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\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 \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\left({x}\right)\right|<{y}\right)$
23 elcnfn ${⊢}ℋ×\left\{0\right\}\in \mathrm{ContFn}↔\left(\left(ℋ×\left\{0\right\}\right):ℋ⟶ℂ\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 \left|\left(ℋ×\left\{0\right\}\right)\left({w}\right)-\left(ℋ×\left\{0\right\}\right)\left({x}\right)\right|<{y}\right)\right)$
24 2 22 23 mpbir2an ${⊢}ℋ×\left\{0\right\}\in \mathrm{ContFn}$