Metamath Proof Explorer

Theorem hhcnf

Description: The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hhcn.1 ${⊢}{D}={norm}_{ℎ}\circ {-}_{ℎ}$
hhcn.2 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
hhcn.4 ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion hhcnf ${⊢}\mathrm{ContFn}={J}\mathrm{Cn}{K}$

Proof

Step Hyp Ref Expression
1 hhcn.1 ${⊢}{D}={norm}_{ℎ}\circ {-}_{ℎ}$
2 hhcn.2 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
3 hhcn.4 ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
4 df-rab ${⊢}\left\{{t}\in \left({ℂ}^{ℋ}\right)|\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right\}=\left\{{t}|\left({t}\in \left({ℂ}^{ℋ}\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)\right\}$
5 df-cnfn ${⊢}\mathrm{ContFn}=\left\{{t}\in \left({ℂ}^{ℋ}\right)|\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right\}$
6 1 hilmetdval ${⊢}\left({x}\in ℋ\wedge {w}\in ℋ\right)\to {x}{D}{w}={norm}_{ℎ}\left({x}{-}_{ℎ}{w}\right)$
7 normsub ${⊢}\left({x}\in ℋ\wedge {w}\in ℋ\right)\to {norm}_{ℎ}\left({x}{-}_{ℎ}{w}\right)={norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
8 6 7 eqtrd ${⊢}\left({x}\in ℋ\wedge {w}\in ℋ\right)\to {x}{D}{w}={norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
9 8 adantll ${⊢}\left(\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to {x}{D}{w}={norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
10 9 breq1d ${⊢}\left(\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left({x}{D}{w}<{z}↔{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\right)$
11 ffvelrn ${⊢}\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\to {t}\left({x}\right)\in ℂ$
12 ffvelrn ${⊢}\left({t}:ℋ⟶ℂ\wedge {w}\in ℋ\right)\to {t}\left({w}\right)\in ℂ$
13 11 12 anim12dan ${⊢}\left({t}:ℋ⟶ℂ\wedge \left({x}\in ℋ\wedge {w}\in ℋ\right)\right)\to \left({t}\left({x}\right)\in ℂ\wedge {t}\left({w}\right)\in ℂ\right)$
14 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
15 14 cnmetdval ${⊢}\left({t}\left({x}\right)\in ℂ\wedge {t}\left({w}\right)\in ℂ\right)\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)=\left|{t}\left({x}\right)-{t}\left({w}\right)\right|$
16 abssub ${⊢}\left({t}\left({x}\right)\in ℂ\wedge {t}\left({w}\right)\in ℂ\right)\to \left|{t}\left({x}\right)-{t}\left({w}\right)\right|=\left|{t}\left({w}\right)-{t}\left({x}\right)\right|$
17 15 16 eqtrd ${⊢}\left({t}\left({x}\right)\in ℂ\wedge {t}\left({w}\right)\in ℂ\right)\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)=\left|{t}\left({w}\right)-{t}\left({x}\right)\right|$
18 13 17 syl ${⊢}\left({t}:ℋ⟶ℂ\wedge \left({x}\in ℋ\wedge {w}\in ℋ\right)\right)\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)=\left|{t}\left({w}\right)-{t}\left({x}\right)\right|$
19 18 anassrs ${⊢}\left(\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)=\left|{t}\left({w}\right)-{t}\left({x}\right)\right|$
20 19 breq1d ${⊢}\left(\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left({t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}↔\left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)$
21 10 20 imbi12d ${⊢}\left(\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left(\left({x}{D}{w}<{z}\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}\right)↔\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)$
22 21 ralbidva ${⊢}\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\to \left(\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({x}{D}{w}<{z}\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}\right)↔\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)$
23 22 rexbidv ${⊢}\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\to \left(\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({x}{D}{w}<{z}\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}\right)↔\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)$
24 23 ralbidv ${⊢}\left({t}:ℋ⟶ℂ\wedge {x}\in ℋ\right)\to \left(\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({x}{D}{w}<{z}\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}\right)↔\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)$
25 24 ralbidva ${⊢}{t}:ℋ⟶ℂ\to \left(\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({x}{D}{w}<{z}\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}\right)↔\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)$
26 25 pm5.32i ${⊢}\left({t}:ℋ⟶ℂ\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({x}{D}{w}<{z}\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}\right)\right)↔\left({t}:ℋ⟶ℂ\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)$
27 1 hilxmet ${⊢}{D}\in \mathrm{\infty Met}\left(ℋ\right)$
28 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
29 3 cnfldtopn ${⊢}{K}=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$
30 2 29 metcn ${⊢}\left({D}\in \mathrm{\infty Met}\left(ℋ\right)\wedge \mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\right)\to \left({t}\in \left({J}\mathrm{Cn}{K}\right)↔\left({t}:ℋ⟶ℂ\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({x}{D}{w}<{z}\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}\right)\right)\right)$
31 27 28 30 mp2an ${⊢}{t}\in \left({J}\mathrm{Cn}{K}\right)↔\left({t}:ℋ⟶ℂ\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({x}{D}{w}<{z}\to {t}\left({x}\right)\left(\mathrm{abs}\circ -\right){t}\left({w}\right)<{y}\right)\right)$
32 cnex ${⊢}ℂ\in \mathrm{V}$
33 ax-hilex ${⊢}ℋ\in \mathrm{V}$
34 32 33 elmap ${⊢}{t}\in \left({ℂ}^{ℋ}\right)↔{t}:ℋ⟶ℂ$
35 34 anbi1i ${⊢}\left({t}\in \left({ℂ}^{ℋ}\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)↔\left({t}:ℋ⟶ℂ\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)$
36 26 31 35 3bitr4i ${⊢}{t}\in \left({J}\mathrm{Cn}{K}\right)↔\left({t}\in \left({ℂ}^{ℋ}\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)$
37 36 abbi2i ${⊢}{J}\mathrm{Cn}{K}=\left\{{t}|\left({t}\in \left({ℂ}^{ℋ}\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|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right)\right\}$
38 4 5 37 3eqtr4i ${⊢}\mathrm{ContFn}={J}\mathrm{Cn}{K}$