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 ⊢ S ∈ BndLinOp
nmoptri.2 ⊢ T ∈ BndLinOp
Assertion adjcoi ⊢ adj h ⁡ S ∘ T = adj h ⁡ T ∘ adj h ⁡ S

Proof

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