# Metamath Proof Explorer

## Theorem hhcno

Description: The continuous operators 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)$
Assertion hhcno ${⊢}\mathrm{ContOp}={J}\mathrm{Cn}{J}$

### Proof

Step Hyp Ref Expression
1 hhcn.1 ${⊢}{D}={norm}_{ℎ}\circ {-}_{ℎ}$
2 hhcn.2 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
3 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 {norm}_{ℎ}\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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)\right\}$
4 df-cnop ${⊢}\mathrm{ContOp}=\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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right\}$
5 1 hilmetdval ${⊢}\left({x}\in ℋ\wedge {w}\in ℋ\right)\to {x}{D}{w}={norm}_{ℎ}\left({x}{-}_{ℎ}{w}\right)$
6 normsub ${⊢}\left({x}\in ℋ\wedge {w}\in ℋ\right)\to {norm}_{ℎ}\left({x}{-}_{ℎ}{w}\right)={norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
7 5 6 eqtrd ${⊢}\left({x}\in ℋ\wedge {w}\in ℋ\right)\to {x}{D}{w}={norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
8 7 adantll ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to {x}{D}{w}={norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
9 8 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)$
10 ffvelrn ${⊢}\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {t}\left({x}\right)\in ℋ$
11 ffvelrn ${⊢}\left({t}:ℋ⟶ℋ\wedge {w}\in ℋ\right)\to {t}\left({w}\right)\in ℋ$
12 10 11 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)$
13 1 hilmetdval ${⊢}\left({t}\left({x}\right)\in ℋ\wedge {t}\left({w}\right)\in ℋ\right)\to {t}\left({x}\right){D}{t}\left({w}\right)={norm}_{ℎ}\left({t}\left({x}\right){-}_{ℎ}{t}\left({w}\right)\right)$
14 normsub ${⊢}\left({t}\left({x}\right)\in ℋ\wedge {t}\left({w}\right)\in ℋ\right)\to {norm}_{ℎ}\left({t}\left({x}\right){-}_{ℎ}{t}\left({w}\right)\right)={norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)$
15 13 14 eqtrd ${⊢}\left({t}\left({x}\right)\in ℋ\wedge {t}\left({w}\right)\in ℋ\right)\to {t}\left({x}\right){D}{t}\left({w}\right)={norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)$
16 12 15 syl ${⊢}\left({t}:ℋ⟶ℋ\wedge \left({x}\in ℋ\wedge {w}\in ℋ\right)\right)\to {t}\left({x}\right){D}{t}\left({w}\right)={norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)$
17 16 anassrs ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to {t}\left({x}\right){D}{t}\left({w}\right)={norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)$
18 17 breq1d ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left({t}\left({x}\right){D}{t}\left({w}\right)<{y}↔{norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)$
19 9 18 imbi12d ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge {w}\in ℋ\right)\to \left(\left({x}{D}{w}<{z}\to {t}\left({x}\right){D}{t}\left({w}\right)<{y}\right)↔\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)$
20 19 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){D}{t}\left({w}\right)<{y}\right)↔\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)$
21 20 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){D}{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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)$
22 21 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){D}{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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)$
23 22 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){D}{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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)$
24 23 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){D}{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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)$
25 1 hilxmet ${⊢}{D}\in \mathrm{\infty Met}\left(ℋ\right)$
26 2 2 metcn ${⊢}\left({D}\in \mathrm{\infty Met}\left(ℋ\right)\wedge {D}\in \mathrm{\infty Met}\left(ℋ\right)\right)\to \left({t}\in \left({J}\mathrm{Cn}{J}\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){D}{t}\left({w}\right)<{y}\right)\right)\right)$
27 25 25 26 mp2an ${⊢}{t}\in \left({J}\mathrm{Cn}{J}\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){D}{t}\left({w}\right)<{y}\right)\right)$
28 ax-hilex ${⊢}ℋ\in \mathrm{V}$
29 28 28 elmap ${⊢}{t}\in \left({ℋ}^{ℋ}\right)↔{t}:ℋ⟶ℋ$
30 29 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 {norm}_{ℎ}\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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)$
31 24 27 30 3bitr4i ${⊢}{t}\in \left({J}\mathrm{Cn}{J}\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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)$
32 31 abbi2i ${⊢}{J}\mathrm{Cn}{J}=\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 {norm}_{ℎ}\left({t}\left({w}\right){-}_{ℎ}{t}\left({x}\right)\right)<{y}\right)\right)\right\}$
33 3 4 32 3eqtr4i ${⊢}\mathrm{ContOp}={J}\mathrm{Cn}{J}$