# 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 𝑆 ∈ BndLinOp
nmoptri.2 𝑇 ∈ BndLinOp

### Proof

Step Hyp Ref Expression
1 nmoptri.1 𝑆 ∈ BndLinOp
2 nmoptri.2 𝑇 ∈ BndLinOp
3 adjbdln ( 𝑇 ∈ BndLinOp → ( adj𝑇 ) ∈ BndLinOp )
4 bdopf ( ( adj𝑇 ) ∈ BndLinOp → ( adj𝑇 ) : ℋ ⟶ ℋ )
5 2 3 4 mp2b ( adj𝑇 ) : ℋ ⟶ ℋ
6 adjbdln ( 𝑆 ∈ BndLinOp → ( adj𝑆 ) ∈ BndLinOp )
7 bdopf ( ( adj𝑆 ) ∈ BndLinOp → ( adj𝑆 ) : ℋ ⟶ ℋ )
8 1 6 7 mp2b ( adj𝑆 ) : ℋ ⟶ ℋ
9 5 8 hocoi ( 𝑦 ∈ ℋ → ( ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) ‘ 𝑦 ) = ( ( adj𝑇 ) ‘ ( ( adj𝑆 ) ‘ 𝑦 ) ) )
10 9 oveq2d ( 𝑦 ∈ ℋ → ( 𝑥 ·ih ( ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( adj𝑇 ) ‘ ( ( adj𝑆 ) ‘ 𝑦 ) ) ) )
11 10 adantl ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( adj𝑇 ) ‘ ( ( adj𝑆 ) ‘ 𝑦 ) ) ) )
12 bdopf ( 𝑆 ∈ BndLinOp → 𝑆 : ℋ ⟶ ℋ )
13 1 12 ax-mp 𝑆 : ℋ ⟶ ℋ
14 bdopf ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
15 2 14 ax-mp 𝑇 : ℋ ⟶ ℋ
16 13 15 hocoi ( 𝑥 ∈ ℋ → ( ( 𝑆𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑇𝑥 ) ) )
17 16 oveq1d ( 𝑥 ∈ ℋ → ( ( ( 𝑆𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑆 ‘ ( 𝑇𝑥 ) ) ·ih 𝑦 ) )
18 17 adantr ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( 𝑆𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( ( 𝑆 ‘ ( 𝑇𝑥 ) ) ·ih 𝑦 ) )
19 15 ffvelrni ( 𝑥 ∈ ℋ → ( 𝑇𝑥 ) ∈ ℋ )
20 bdopadj ( 𝑆 ∈ BndLinOp → 𝑆 ∈ dom adj )
21 1 20 ax-mp 𝑆 ∈ dom adj
22 adj2 ( ( 𝑆 ∈ dom adj ∧ ( 𝑇𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆 ‘ ( 𝑇𝑥 ) ) ·ih 𝑦 ) = ( ( 𝑇𝑥 ) ·ih ( ( adj𝑆 ) ‘ 𝑦 ) ) )
23 21 22 mp3an1 ( ( ( 𝑇𝑥 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆 ‘ ( 𝑇𝑥 ) ) ·ih 𝑦 ) = ( ( 𝑇𝑥 ) ·ih ( ( adj𝑆 ) ‘ 𝑦 ) ) )
24 19 23 sylan ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑆 ‘ ( 𝑇𝑥 ) ) ·ih 𝑦 ) = ( ( 𝑇𝑥 ) ·ih ( ( adj𝑆 ) ‘ 𝑦 ) ) )
25 8 ffvelrni ( 𝑦 ∈ ℋ → ( ( adj𝑆 ) ‘ 𝑦 ) ∈ ℋ )
26 bdopadj ( 𝑇 ∈ BndLinOp → 𝑇 ∈ dom adj )
27 2 26 ax-mp 𝑇 ∈ dom adj
28 adj2 ( ( 𝑇 ∈ dom adj𝑥 ∈ ℋ ∧ ( ( adj𝑆 ) ‘ 𝑦 ) ∈ ℋ ) → ( ( 𝑇𝑥 ) ·ih ( ( adj𝑆 ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( adj𝑇 ) ‘ ( ( adj𝑆 ) ‘ 𝑦 ) ) ) )
29 27 28 mp3an1 ( ( 𝑥 ∈ ℋ ∧ ( ( adj𝑆 ) ‘ 𝑦 ) ∈ ℋ ) → ( ( 𝑇𝑥 ) ·ih ( ( adj𝑆 ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( adj𝑇 ) ‘ ( ( adj𝑆 ) ‘ 𝑦 ) ) ) )
30 25 29 sylan2 ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇𝑥 ) ·ih ( ( adj𝑆 ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( adj𝑇 ) ‘ ( ( adj𝑆 ) ‘ 𝑦 ) ) ) )
31 18 24 30 3eqtrd ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( 𝑆𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adj𝑇 ) ‘ ( ( adj𝑆 ) ‘ 𝑦 ) ) ) )
32 1 2 bdopcoi ( 𝑆𝑇 ) ∈ BndLinOp
33 bdopadj ( ( 𝑆𝑇 ) ∈ BndLinOp → ( 𝑆𝑇 ) ∈ dom adj )
34 32 33 ax-mp ( 𝑆𝑇 ) ∈ dom adj
35 adj2 ( ( ( 𝑆𝑇 ) ∈ dom adj𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( 𝑆𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adj ‘ ( 𝑆𝑇 ) ) ‘ 𝑦 ) ) )
36 34 35 mp3an1 ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( 𝑆𝑇 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( adj ‘ ( 𝑆𝑇 ) ) ‘ 𝑦 ) ) )
37 11 31 36 3eqtr2rd ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( ( adj ‘ ( 𝑆𝑇 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) ‘ 𝑦 ) ) )
38 37 rgen2 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( ( adj ‘ ( 𝑆𝑇 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) ‘ 𝑦 ) )
39 adjbdln ( ( 𝑆𝑇 ) ∈ BndLinOp → ( adj ‘ ( 𝑆𝑇 ) ) ∈ BndLinOp )
40 bdopf ( ( adj ‘ ( 𝑆𝑇 ) ) ∈ BndLinOp → ( adj ‘ ( 𝑆𝑇 ) ) : ℋ ⟶ ℋ )
41 32 39 40 mp2b ( adj ‘ ( 𝑆𝑇 ) ) : ℋ ⟶ ℋ
42 5 8 hocofi ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) : ℋ ⟶ ℋ
43 hoeq2 ( ( ( adj ‘ ( 𝑆𝑇 ) ) : ℋ ⟶ ℋ ∧ ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( ( adj ‘ ( 𝑆𝑇 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) ‘ 𝑦 ) ) ↔ ( adj ‘ ( 𝑆𝑇 ) ) = ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) ) )
44 41 42 43 mp2an ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( ( adj ‘ ( 𝑆𝑇 ) ) ‘ 𝑦 ) ) = ( 𝑥 ·ih ( ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) ‘ 𝑦 ) ) ↔ ( adj ‘ ( 𝑆𝑇 ) ) = ( ( adj𝑇 ) ∘ ( adj𝑆 ) ) )
45 38 44 mpbi ( adj ‘ ( 𝑆𝑇 ) ) = ( ( adj𝑇 ) ∘ ( adj𝑆 ) )