# Metamath Proof Explorer

Description: Every continuous linear Hilbert space operator has an adjoint. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion cnlnssadj ${⊢}\mathrm{LinOp}\cap \mathrm{ContOp}\subseteq \mathrm{dom}{adj}_{h}$

### Proof

Step Hyp Ref Expression
1 cnlnadj ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)$
2 df-rex ${⊢}\exists {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)↔\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\right)$
3 1 2 sylib ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists {t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\right)$
4 inss1 ${⊢}\mathrm{LinOp}\cap \mathrm{ContOp}\subseteq \mathrm{LinOp}$
5 4 sseli ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to {y}\in \mathrm{LinOp}$
6 lnopf ${⊢}{y}\in \mathrm{LinOp}\to {y}:ℋ⟶ℋ$
7 5 6 syl ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to {y}:ℋ⟶ℋ$
8 7 a1d ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left(\left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\right)\to {y}:ℋ⟶ℋ\right)$
9 4 sseli ${⊢}{t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to {t}\in \mathrm{LinOp}$
10 lnopf ${⊢}{t}\in \mathrm{LinOp}\to {t}:ℋ⟶ℋ$
11 9 10 syl ${⊢}{t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to {t}:ℋ⟶ℋ$
12 11 a1i ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to {t}:ℋ⟶ℋ\right)$
13 12 adantrd ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left(\left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\right)\to {t}:ℋ⟶ℋ\right)$
14 eqcom ${⊢}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)↔{x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)={y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}$
15 14 biimpi ${⊢}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\to {x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)={y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}$
16 15 2ralimi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)={y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}$
17 adjsym ${⊢}\left({t}:ℋ⟶ℋ\wedge {y}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)={y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
18 11 7 17 syl2anr ${⊢}\left({y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)={y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
19 16 18 syl5ib ${⊢}\left({y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
20 19 expimpd ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left(\left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
21 8 13 20 3jcad ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left(\left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\right)\to \left({y}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)\right)$
22 dfadj2 ${⊢}{adj}_{h}=\left\{⟨{u},{v}⟩|\left({u}:ℋ⟶ℋ\wedge {v}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)\right\}$
23 22 eleq2i ${⊢}⟨{y},{t}⟩\in {adj}_{h}↔⟨{y},{t}⟩\in \left\{⟨{u},{v}⟩|\left({u}:ℋ⟶ℋ\wedge {v}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)\right\}$
24 vex ${⊢}{y}\in \mathrm{V}$
25 vex ${⊢}{t}\in \mathrm{V}$
26 feq1 ${⊢}{u}={y}\to \left({u}:ℋ⟶ℋ↔{y}:ℋ⟶ℋ\right)$
27 fveq1 ${⊢}{u}={y}\to {u}\left({z}\right)={y}\left({z}\right)$
28 27 oveq2d ${⊢}{u}={y}\to {x}{\cdot }_{\mathrm{ih}}{u}\left({z}\right)={x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)$
29 28 eqeq1d ${⊢}{u}={y}\to \left({x}{\cdot }_{\mathrm{ih}}{u}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}↔{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
30 29 2ralbidv ${⊢}{u}={y}\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
31 26 30 3anbi13d ${⊢}{u}={y}\to \left(\left({u}:ℋ⟶ℋ\wedge {v}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)↔\left({y}:ℋ⟶ℋ\wedge {v}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)\right)$
32 feq1 ${⊢}{v}={t}\to \left({v}:ℋ⟶ℋ↔{t}:ℋ⟶ℋ\right)$
33 fveq1 ${⊢}{v}={t}\to {v}\left({x}\right)={t}\left({x}\right)$
34 33 oveq1d ${⊢}{v}={t}\to {v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}$
35 34 eqeq2d ${⊢}{v}={t}\to \left({x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}↔{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
36 35 2ralbidv ${⊢}{v}={t}\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
37 32 36 3anbi23d ${⊢}{v}={t}\to \left(\left({y}:ℋ⟶ℋ\wedge {v}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)↔\left({y}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)\right)$
38 24 25 31 37 opelopab ${⊢}⟨{y},{t}⟩\in \left\{⟨{u},{v}⟩|\left({u}:ℋ⟶ℋ\wedge {v}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({z}\right)={v}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)\right\}↔\left({y}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)$
39 23 38 bitr2i ${⊢}\left({y}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}\left({z}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{z}\right)↔⟨{y},{t}⟩\in {adj}_{h}$
40 21 39 syl6ib ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left(\left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\right)\to ⟨{y},{t}⟩\in {adj}_{h}\right)$
41 40 eximdv ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{y}\left({x}\right){\cdot }_{\mathrm{ih}}{z}={x}{\cdot }_{\mathrm{ih}}{t}\left({z}\right)\right)\to \exists {t}\phantom{\rule{.4em}{0ex}}⟨{y},{t}⟩\in {adj}_{h}\right)$
42 3 41 mpd ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists {t}\phantom{\rule{.4em}{0ex}}⟨{y},{t}⟩\in {adj}_{h}$
43 24 eldm2 ${⊢}{y}\in \mathrm{dom}{adj}_{h}↔\exists {t}\phantom{\rule{.4em}{0ex}}⟨{y},{t}⟩\in {adj}_{h}$
44 42 43 sylibr ${⊢}{y}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to {y}\in \mathrm{dom}{adj}_{h}$
45 44 ssriv ${⊢}\mathrm{LinOp}\cap \mathrm{ContOp}\subseteq \mathrm{dom}{adj}_{h}$