# Metamath Proof Explorer

Description: The adjoint of a composition of bounded linear operators. Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nmoptri.1 ${⊢}{S}\in \mathrm{BndLinOp}$
nmoptri.2 ${⊢}{T}\in \mathrm{BndLinOp}$
Assertion adjcoi ${⊢}{adj}_{h}\left({S}\circ {T}\right)={adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 nmoptri.1 ${⊢}{S}\in \mathrm{BndLinOp}$
2 nmoptri.2 ${⊢}{T}\in \mathrm{BndLinOp}$
3 adjbdln ${⊢}{T}\in \mathrm{BndLinOp}\to {adj}_{h}\left({T}\right)\in \mathrm{BndLinOp}$
4 bdopf ${⊢}{adj}_{h}\left({T}\right)\in \mathrm{BndLinOp}\to {adj}_{h}\left({T}\right):ℋ⟶ℋ$
5 2 3 4 mp2b ${⊢}{adj}_{h}\left({T}\right):ℋ⟶ℋ$
6 adjbdln ${⊢}{S}\in \mathrm{BndLinOp}\to {adj}_{h}\left({S}\right)\in \mathrm{BndLinOp}$
7 bdopf ${⊢}{adj}_{h}\left({S}\right)\in \mathrm{BndLinOp}\to {adj}_{h}\left({S}\right):ℋ⟶ℋ$
8 1 6 7 mp2b ${⊢}{adj}_{h}\left({S}\right):ℋ⟶ℋ$
9 5 8 hocoi ${⊢}{y}\in ℋ\to \left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right)\left({y}\right)={adj}_{h}\left({T}\right)\left({adj}_{h}\left({S}\right)\left({y}\right)\right)$
10 9 oveq2d ${⊢}{y}\in ℋ\to {x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({adj}_{h}\left({S}\right)\left({y}\right)\right)$
11 10 adantl ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({adj}_{h}\left({S}\right)\left({y}\right)\right)$
12 bdopf ${⊢}{S}\in \mathrm{BndLinOp}\to {S}:ℋ⟶ℋ$
13 1 12 ax-mp ${⊢}{S}:ℋ⟶ℋ$
14 bdopf ${⊢}{T}\in \mathrm{BndLinOp}\to {T}:ℋ⟶ℋ$
15 2 14 ax-mp ${⊢}{T}:ℋ⟶ℋ$
16 13 15 hocoi ${⊢}{x}\in ℋ\to \left({S}\circ {T}\right)\left({x}\right)={S}\left({T}\left({x}\right)\right)$
17 16 oveq1d ${⊢}{x}\in ℋ\to \left({S}\circ {T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={S}\left({T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
18 17 adantr ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \left({S}\circ {T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={S}\left({T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}$
19 15 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
20 bdopadj ${⊢}{S}\in \mathrm{BndLinOp}\to {S}\in \mathrm{dom}{adj}_{h}$
21 1 20 ax-mp ${⊢}{S}\in \mathrm{dom}{adj}_{h}$
22 adj2 ${⊢}\left({S}\in \mathrm{dom}{adj}_{h}\wedge {T}\left({x}\right)\in ℋ\wedge {y}\in ℋ\right)\to {S}\left({T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)$
23 21 22 mp3an1 ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {y}\in ℋ\right)\to {S}\left({T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)$
24 19 23 sylan ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {S}\left({T}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)$
25 8 ffvelrni ${⊢}{y}\in ℋ\to {adj}_{h}\left({S}\right)\left({y}\right)\in ℋ$
26 bdopadj ${⊢}{T}\in \mathrm{BndLinOp}\to {T}\in \mathrm{dom}{adj}_{h}$
27 2 26 ax-mp ${⊢}{T}\in \mathrm{dom}{adj}_{h}$
28 adj2 ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {adj}_{h}\left({S}\right)\left({y}\right)\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({adj}_{h}\left({S}\right)\left({y}\right)\right)$
29 27 28 mp3an1 ${⊢}\left({x}\in ℋ\wedge {adj}_{h}\left({S}\right)\left({y}\right)\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({adj}_{h}\left({S}\right)\left({y}\right)\right)$
30 25 29 sylan2 ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({adj}_{h}\left({S}\right)\left({y}\right)\right)$
31 18 24 30 3eqtrd ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \left({S}\circ {T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({T}\right)\left({adj}_{h}\left({S}\right)\left({y}\right)\right)$
32 1 2 bdopcoi ${⊢}{S}\circ {T}\in \mathrm{BndLinOp}$
33 bdopadj ${⊢}{S}\circ {T}\in \mathrm{BndLinOp}\to {S}\circ {T}\in \mathrm{dom}{adj}_{h}$
34 32 33 ax-mp ${⊢}{S}\circ {T}\in \mathrm{dom}{adj}_{h}$
35 adj2 ${⊢}\left({S}\circ {T}\in \mathrm{dom}{adj}_{h}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to \left({S}\circ {T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\circ {T}\right)\left({y}\right)$
36 34 35 mp3an1 ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \left({S}\circ {T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\circ {T}\right)\left({y}\right)$
37 11 31 36 3eqtr2rd ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\circ {T}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right)\left({y}\right)$
38 37 rgen2 ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\circ {T}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right)\left({y}\right)$
39 adjbdln ${⊢}{S}\circ {T}\in \mathrm{BndLinOp}\to {adj}_{h}\left({S}\circ {T}\right)\in \mathrm{BndLinOp}$
40 bdopf ${⊢}{adj}_{h}\left({S}\circ {T}\right)\in \mathrm{BndLinOp}\to {adj}_{h}\left({S}\circ {T}\right):ℋ⟶ℋ$
41 32 39 40 mp2b ${⊢}{adj}_{h}\left({S}\circ {T}\right):ℋ⟶ℋ$
42 5 8 hocofi ${⊢}\left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right):ℋ⟶ℋ$
43 hoeq2 ${⊢}\left({adj}_{h}\left({S}\circ {T}\right):ℋ⟶ℋ\wedge \left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right):ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\circ {T}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right)\left({y}\right)↔{adj}_{h}\left({S}\circ {T}\right)={adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right)$
44 41 42 43 mp2an ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{adj}_{h}\left({S}\circ {T}\right)\left({y}\right)={x}{\cdot }_{\mathrm{ih}}\left({adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)\right)\left({y}\right)↔{adj}_{h}\left({S}\circ {T}\right)={adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)$
45 38 44 mpbi ${⊢}{adj}_{h}\left({S}\circ {T}\right)={adj}_{h}\left({T}\right)\circ {adj}_{h}\left({S}\right)$