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 ⊢ 𝑆 ∈ BndLinOp
nmoptri.2 ⊢ 𝑇 ∈ BndLinOp
Assertion adjcoi ( adjℎ ‘ ( 𝑆 ∘ 𝑇 ) ) = ( ( adjℎ ‘ 𝑇 ) ∘ ( adjℎ ‘ 𝑆 ) )

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 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
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 ffvelcdmi ⊢ ( 𝑦 ∈ ℋ → ( ( 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ℎ ‘ 𝑆 ) )