Metamath Proof Explorer


Theorem adjcoi

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 SBndLinOp
nmoptri.2 TBndLinOp
Assertion adjcoi adjhST=adjhTadjhS

Proof

Step Hyp Ref Expression
1 nmoptri.1 SBndLinOp
2 nmoptri.2 TBndLinOp
3 adjbdln TBndLinOpadjhTBndLinOp
4 bdopf adjhTBndLinOpadjhT:
5 2 3 4 mp2b adjhT:
6 adjbdln SBndLinOpadjhSBndLinOp
7 bdopf adjhSBndLinOpadjhS:
8 1 6 7 mp2b adjhS:
9 5 8 hocoi yadjhTadjhSy=adjhTadjhSy
10 9 oveq2d yxihadjhTadjhSy=xihadjhTadjhSy
11 10 adantl xyxihadjhTadjhSy=xihadjhTadjhSy
12 bdopf SBndLinOpS:
13 1 12 ax-mp S:
14 bdopf TBndLinOpT:
15 2 14 ax-mp T:
16 13 15 hocoi xSTx=STx
17 16 oveq1d xSTxihy=STxihy
18 17 adantr xySTxihy=STxihy
19 15 ffvelrni xTx
20 bdopadj SBndLinOpSdomadjh
21 1 20 ax-mp Sdomadjh
22 adj2 SdomadjhTxySTxihy=TxihadjhSy
23 21 22 mp3an1 TxySTxihy=TxihadjhSy
24 19 23 sylan xySTxihy=TxihadjhSy
25 8 ffvelrni yadjhSy
26 bdopadj TBndLinOpTdomadjh
27 2 26 ax-mp Tdomadjh
28 adj2 TdomadjhxadjhSyTxihadjhSy=xihadjhTadjhSy
29 27 28 mp3an1 xadjhSyTxihadjhSy=xihadjhTadjhSy
30 25 29 sylan2 xyTxihadjhSy=xihadjhTadjhSy
31 18 24 30 3eqtrd xySTxihy=xihadjhTadjhSy
32 1 2 bdopcoi STBndLinOp
33 bdopadj STBndLinOpSTdomadjh
34 32 33 ax-mp STdomadjh
35 adj2 STdomadjhxySTxihy=xihadjhSTy
36 34 35 mp3an1 xySTxihy=xihadjhSTy
37 11 31 36 3eqtr2rd xyxihadjhSTy=xihadjhTadjhSy
38 37 rgen2 xyxihadjhSTy=xihadjhTadjhSy
39 adjbdln STBndLinOpadjhSTBndLinOp
40 bdopf adjhSTBndLinOpadjhST:
41 32 39 40 mp2b adjhST:
42 5 8 hocofi adjhTadjhS:
43 hoeq2 adjhST:adjhTadjhS:xyxihadjhSTy=xihadjhTadjhSyadjhST=adjhTadjhS
44 41 42 43 mp2an xyxihadjhSTy=xihadjhTadjhSyadjhST=adjhTadjhS
45 38 44 mpbi adjhST=adjhTadjhS