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 | |
|
nmoptri.2 | |
||
Assertion | adjcoi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmoptri.1 | |
|
2 | nmoptri.2 | |
|
3 | adjbdln | |
|
4 | bdopf | |
|
5 | 2 3 4 | mp2b | |
6 | adjbdln | |
|
7 | bdopf | |
|
8 | 1 6 7 | mp2b | |
9 | 5 8 | hocoi | |
10 | 9 | oveq2d | |
11 | 10 | adantl | |
12 | bdopf | |
|
13 | 1 12 | ax-mp | |
14 | bdopf | |
|
15 | 2 14 | ax-mp | |
16 | 13 15 | hocoi | |
17 | 16 | oveq1d | |
18 | 17 | adantr | |
19 | 15 | ffvelrni | |
20 | bdopadj | |
|
21 | 1 20 | ax-mp | |
22 | adj2 | |
|
23 | 21 22 | mp3an1 | |
24 | 19 23 | sylan | |
25 | 8 | ffvelrni | |
26 | bdopadj | |
|
27 | 2 26 | ax-mp | |
28 | adj2 | |
|
29 | 27 28 | mp3an1 | |
30 | 25 29 | sylan2 | |
31 | 18 24 30 | 3eqtrd | |
32 | 1 2 | bdopcoi | |
33 | bdopadj | |
|
34 | 32 33 | ax-mp | |
35 | adj2 | |
|
36 | 34 35 | mp3an1 | |
37 | 11 31 36 | 3eqtr2rd | |
38 | 37 | rgen2 | |
39 | adjbdln | |
|
40 | bdopf | |
|
41 | 32 39 40 | mp2b | |
42 | 5 8 | hocofi | |
43 | hoeq2 | |
|
44 | 41 42 43 | mp2an | |
45 | 38 44 | mpbi | |