Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  adjcoi Structured version   Visualization version   GIF version

 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.)
Hypotheses
Ref Expression
nmoptri.1 𝑆 ∈ BndLinOp
nmoptri.2 𝑇 ∈ BndLinOp
Assertion
Ref Expression

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nmoptri.2 . . . . . . . 8 𝑇 ∈ BndLinOp
2 adjbdln 28326 . . . . . . . 8 (𝑇 ∈ BndLinOp → (adj𝑇) ∈ BndLinOp)
3 bdopf 28105 . . . . . . . 8 ((adj𝑇) ∈ BndLinOp → (adj𝑇): ℋ⟶ ℋ)
41, 2, 3mp2b 10 . . . . . . 7 (adj𝑇): ℋ⟶ ℋ
5 nmoptri.1 . . . . . . . 8 𝑆 ∈ BndLinOp
6 adjbdln 28326 . . . . . . . 8 (𝑆 ∈ BndLinOp → (adj𝑆) ∈ BndLinOp)
7 bdopf 28105 . . . . . . . 8 ((adj𝑆) ∈ BndLinOp → (adj𝑆): ℋ⟶ ℋ)
85, 6, 7mp2b 10 . . . . . . 7 (adj𝑆): ℋ⟶ ℋ
12 bdopf 28105 . . . . . . . . 9 (𝑆 ∈ BndLinOp → 𝑆: ℋ⟶ ℋ)
135, 12ax-mp 5 . . . . . . . 8 𝑆: ℋ⟶ ℋ
14 bdopf 28105 . . . . . . . . 9 (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ)
151, 14ax-mp 5 . . . . . . . 8 𝑇: ℋ⟶ ℋ
1613, 15hocoi 28007 . . . . . . 7 (𝑥 ∈ ℋ → ((𝑆𝑇)‘𝑥) = (𝑆‘(𝑇𝑥)))
1716oveq1d 6564 . . . . . 6 (𝑥 ∈ ℋ → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = ((𝑆‘(𝑇𝑥)) ·ih 𝑦))
1817adantr 480 . . . . 5 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = ((𝑆‘(𝑇𝑥)) ·ih 𝑦))
1915ffvelrni 6266 . . . . . 6 (𝑥 ∈ ℋ → (𝑇𝑥) ∈ ℋ)
20 bdopadj 28325 . . . . . . . 8 (𝑆 ∈ BndLinOp → 𝑆 ∈ dom adj)
215, 20ax-mp 5 . . . . . . 7 𝑆 ∈ dom adj
22 adj2 28177 . . . . . . 7 ((𝑆 ∈ dom adj ∧ (𝑇𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇𝑥)) ·ih 𝑦) = ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)))
2321, 22mp3an1 1403 . . . . . 6 (((𝑇𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇𝑥)) ·ih 𝑦) = ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)))
2419, 23sylan 487 . . . . 5 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇𝑥)) ·ih 𝑦) = ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)))
258ffvelrni 6266 . . . . . 6 (𝑦 ∈ ℋ → ((adj𝑆)‘𝑦) ∈ ℋ)
26 bdopadj 28325 . . . . . . . 8 (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adj)
271, 26ax-mp 5 . . . . . . 7 𝑇 ∈ dom adj
2927, 28mp3an1 1403 . . . . . 6 ((𝑥 ∈ ℋ ∧ ((adj𝑆)‘𝑦) ∈ ℋ) → ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
3025, 29sylan2 490 . . . . 5 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
3118, 24, 303eqtrd 2648 . . . 4 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
325, 1bdopcoi 28341 . . . . . 6 (𝑆𝑇) ∈ BndLinOp
33 bdopadj 28325 . . . . . 6 ((𝑆𝑇) ∈ BndLinOp → (𝑆𝑇) ∈ dom adj)
3432, 33ax-mp 5 . . . . 5 (𝑆𝑇) ∈ dom adj
35 adj2 28177 . . . . 5 (((𝑆𝑇) ∈ dom adj𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)))
3634, 35mp3an1 1403 . . . 4 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)))
3711, 31, 363eqtr2rd 2651 . . 3 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)) = (𝑥 ·ih (((adj𝑇) ∘ (adj𝑆))‘𝑦)))
3837rgen2a 2960 . 2 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)) = (𝑥 ·ih (((adj𝑇) ∘ (adj𝑆))‘𝑦))
39 adjbdln 28326 . . . 4 ((𝑆𝑇) ∈ BndLinOp → (adj‘(𝑆𝑇)) ∈ BndLinOp)
40 bdopf 28105 . . . 4 ((adj‘(𝑆𝑇)) ∈ BndLinOp → (adj‘(𝑆𝑇)): ℋ⟶ ℋ)
4132, 39, 40mp2b 10 . . 3 (adj‘(𝑆𝑇)): ℋ⟶ ℋ