# Metamath Proof Explorer

Description: The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjbdln ${⊢}{T}\in \mathrm{BndLinOp}\to {adj}_{h}\left({T}\right)\in \mathrm{BndLinOp}$

### Proof

Step Hyp Ref Expression
1 bdopadj ${⊢}{T}\in \mathrm{BndLinOp}\to {T}\in \mathrm{dom}{adj}_{h}$
2 adjval ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to {adj}_{h}\left({T}\right)=\left(\iota {t}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
3 1 2 syl ${⊢}{T}\in \mathrm{BndLinOp}\to {adj}_{h}\left({T}\right)=\left(\iota {t}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
4 cnlnadj ${⊢}{T}\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 {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$
5 lncnopbd ${⊢}{T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)↔{T}\in \mathrm{BndLinOp}$
6 lncnbd ${⊢}\mathrm{LinOp}\cap \mathrm{ContOp}=\mathrm{BndLinOp}$
7 6 rexeqi ${⊢}\exists {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)↔\exists {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$
8 4 5 7 3imtr3i ${⊢}{T}\in \mathrm{BndLinOp}\to \exists {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$
9 bdopf ${⊢}{T}\in \mathrm{BndLinOp}\to {T}:ℋ⟶ℋ$
10 bdopf ${⊢}{t}\in \mathrm{BndLinOp}\to {t}:ℋ⟶ℋ$
11 adjsym ${⊢}\left({T}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
12 9 10 11 syl2an ${⊢}\left({T}\in \mathrm{BndLinOp}\wedge {t}\in \mathrm{BndLinOp}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
13 eqcom ${⊢}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)↔{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
14 13 2ralbii ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
15 12 14 syl6bbr ${⊢}\left({T}\in \mathrm{BndLinOp}\wedge {t}\in \mathrm{BndLinOp}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)\right)$
16 15 rexbidva ${⊢}{T}\in \mathrm{BndLinOp}\to \left(\exists {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\exists {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)\right)$
17 8 16 mpbird ${⊢}{T}\in \mathrm{BndLinOp}\to \exists {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
18 adjeu ${⊢}{T}:ℋ⟶ℋ\to \left({T}\in \mathrm{dom}{adj}_{h}↔\exists !{t}\in \left({ℋ}^{ℋ}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
19 9 18 syl ${⊢}{T}\in \mathrm{BndLinOp}\to \left({T}\in \mathrm{dom}{adj}_{h}↔\exists !{t}\in \left({ℋ}^{ℋ}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
20 1 19 mpbid ${⊢}{T}\in \mathrm{BndLinOp}\to \exists !{t}\in \left({ℋ}^{ℋ}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
21 ax-hilex ${⊢}ℋ\in \mathrm{V}$
22 21 21 elmap ${⊢}{t}\in \left({ℋ}^{ℋ}\right)↔{t}:ℋ⟶ℋ$
23 10 22 sylibr ${⊢}{t}\in \mathrm{BndLinOp}\to {t}\in \left({ℋ}^{ℋ}\right)$
24 23 ssriv ${⊢}\mathrm{BndLinOp}\subseteq {ℋ}^{ℋ}$
25 id ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
26 25 rgenw ${⊢}\forall {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
27 riotass2 ${⊢}\left(\left(\mathrm{BndLinOp}\subseteq {ℋ}^{ℋ}\wedge \forall {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)\wedge \left(\exists {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\wedge \exists !{t}\in \left({ℋ}^{ℋ}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)\to \left(\iota {t}\in \mathrm{BndLinOp}|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)=\left(\iota {t}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
28 24 26 27 mpanl12 ${⊢}\left(\exists {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\wedge \exists !{t}\in \left({ℋ}^{ℋ}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\to \left(\iota {t}\in \mathrm{BndLinOp}|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)=\left(\iota {t}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
29 17 20 28 syl2anc ${⊢}{T}\in \mathrm{BndLinOp}\to \left(\iota {t}\in \mathrm{BndLinOp}|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)=\left(\iota {t}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
30 3 29 eqtr4d ${⊢}{T}\in \mathrm{BndLinOp}\to {adj}_{h}\left({T}\right)=\left(\iota {t}\in \mathrm{BndLinOp}|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
31 24 a1i ${⊢}{T}\in \mathrm{BndLinOp}\to \mathrm{BndLinOp}\subseteq {ℋ}^{ℋ}$
32 reuss ${⊢}\left(\mathrm{BndLinOp}\subseteq {ℋ}^{ℋ}\wedge \exists {t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\wedge \exists !{t}\in \left({ℋ}^{ℋ}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\to \exists !{t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
33 31 17 20 32 syl3anc ${⊢}{T}\in \mathrm{BndLinOp}\to \exists !{t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
34 riotacl ${⊢}\exists !{t}\in \mathrm{BndLinOp}\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\to \left(\iota {t}\in \mathrm{BndLinOp}|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\in \mathrm{BndLinOp}$
35 33 34 syl ${⊢}{T}\in \mathrm{BndLinOp}\to \left(\iota {t}\in \mathrm{BndLinOp}|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\in \mathrm{BndLinOp}$
36 30 35 eqeltrd ${⊢}{T}\in \mathrm{BndLinOp}\to {adj}_{h}\left({T}\right)\in \mathrm{BndLinOp}$