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

Proof of Theorem adjcoi
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nmoptri.2 . . . . . . . 8 𝑇 ∈ BndLinOp
2 adjbdln 29070 . . . . . . . 8 (𝑇 ∈ BndLinOp → (adj𝑇) ∈ BndLinOp)
3 bdopf 28849 . . . . . . . 8 ((adj𝑇) ∈ BndLinOp → (adj𝑇): ℋ⟶ ℋ)
41, 2, 3mp2b 10 . . . . . . 7 (adj𝑇): ℋ⟶ ℋ
5 nmoptri.1 . . . . . . . 8 𝑆 ∈ BndLinOp
6 adjbdln 29070 . . . . . . . 8 (𝑆 ∈ BndLinOp → (adj𝑆) ∈ BndLinOp)
7 bdopf 28849 . . . . . . . 8 ((adj𝑆) ∈ BndLinOp → (adj𝑆): ℋ⟶ ℋ)
85, 6, 7mp2b 10 . . . . . . 7 (adj𝑆): ℋ⟶ ℋ
94, 8hocoi 28751 . . . . . 6 (𝑦 ∈ ℋ → (((adj𝑇) ∘ (adj𝑆))‘𝑦) = ((adj𝑇)‘((adj𝑆)‘𝑦)))
109oveq2d 6706 . . . . 5 (𝑦 ∈ ℋ → (𝑥 ·ih (((adj𝑇) ∘ (adj𝑆))‘𝑦)) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
1110adantl 481 . . . 4 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·ih (((adj𝑇) ∘ (adj𝑆))‘𝑦)) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
12 bdopf 28849 . . . . . . . . 9 (𝑆 ∈ BndLinOp → 𝑆: ℋ⟶ ℋ)
135, 12ax-mp 5 . . . . . . . 8 𝑆: ℋ⟶ ℋ
14 bdopf 28849 . . . . . . . . 9 (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ)
151, 14ax-mp 5 . . . . . . . 8 𝑇: ℋ⟶ ℋ
1613, 15hocoi 28751 . . . . . . 7 (𝑥 ∈ ℋ → ((𝑆𝑇)‘𝑥) = (𝑆‘(𝑇𝑥)))
1716oveq1d 6705 . . . . . 6 (𝑥 ∈ ℋ → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = ((𝑆‘(𝑇𝑥)) ·ih 𝑦))
1817adantr 480 . . . . 5 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = ((𝑆‘(𝑇𝑥)) ·ih 𝑦))
1915ffvelrni 6398 . . . . . 6 (𝑥 ∈ ℋ → (𝑇𝑥) ∈ ℋ)
20 bdopadj 29069 . . . . . . . 8 (𝑆 ∈ BndLinOp → 𝑆 ∈ dom adj)
215, 20ax-mp 5 . . . . . . 7 𝑆 ∈ dom adj
22 adj2 28921 . . . . . . 7 ((𝑆 ∈ dom adj ∧ (𝑇𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇𝑥)) ·ih 𝑦) = ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)))
2321, 22mp3an1 1451 . . . . . 6 (((𝑇𝑥) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇𝑥)) ·ih 𝑦) = ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)))
2419, 23sylan 487 . . . . 5 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑆‘(𝑇𝑥)) ·ih 𝑦) = ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)))
258ffvelrni 6398 . . . . . 6 (𝑦 ∈ ℋ → ((adj𝑆)‘𝑦) ∈ ℋ)
26 bdopadj 29069 . . . . . . . 8 (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adj)
271, 26ax-mp 5 . . . . . . 7 𝑇 ∈ dom adj
28 adj2 28921 . . . . . . 7 ((𝑇 ∈ dom adj𝑥 ∈ ℋ ∧ ((adj𝑆)‘𝑦) ∈ ℋ) → ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
2927, 28mp3an1 1451 . . . . . 6 ((𝑥 ∈ ℋ ∧ ((adj𝑆)‘𝑦) ∈ ℋ) → ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
3025, 29sylan2 490 . . . . 5 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑥) ·ih ((adj𝑆)‘𝑦)) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
3118, 24, 303eqtrd 2689 . . . 4 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj𝑇)‘((adj𝑆)‘𝑦))))
325, 1bdopcoi 29085 . . . . . 6 (𝑆𝑇) ∈ BndLinOp
33 bdopadj 29069 . . . . . 6 ((𝑆𝑇) ∈ BndLinOp → (𝑆𝑇) ∈ dom adj)
3432, 33ax-mp 5 . . . . 5 (𝑆𝑇) ∈ dom adj
35 adj2 28921 . . . . 5 (((𝑆𝑇) ∈ dom adj𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)))
3634, 35mp3an1 1451 . . . 4 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑆𝑇)‘𝑥) ·ih 𝑦) = (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)))
3711, 31, 363eqtr2rd 2692 . . 3 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)) = (𝑥 ·ih (((adj𝑇) ∘ (adj𝑆))‘𝑦)))
3837rgen2a 3006 . 2 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)) = (𝑥 ·ih (((adj𝑇) ∘ (adj𝑆))‘𝑦))
39 adjbdln 29070 . . . 4 ((𝑆𝑇) ∈ BndLinOp → (adj‘(𝑆𝑇)) ∈ BndLinOp)
40 bdopf 28849 . . . 4 ((adj‘(𝑆𝑇)) ∈ BndLinOp → (adj‘(𝑆𝑇)): ℋ⟶ ℋ)
4132, 39, 40mp2b 10 . . 3 (adj‘(𝑆𝑇)): ℋ⟶ ℋ
424, 8hocofi 28753 . . 3 ((adj𝑇) ∘ (adj𝑆)): ℋ⟶ ℋ
43 hoeq2 28818 . . 3 (((adj‘(𝑆𝑇)): ℋ⟶ ℋ ∧ ((adj𝑇) ∘ (adj𝑆)): ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)) = (𝑥 ·ih (((adj𝑇) ∘ (adj𝑆))‘𝑦)) ↔ (adj‘(𝑆𝑇)) = ((adj𝑇) ∘ (adj𝑆))))
4441, 42, 43mp2an 708 . 2 (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih ((adj‘(𝑆𝑇))‘𝑦)) = (𝑥 ·ih (((adj𝑇) ∘ (adj𝑆))‘𝑦)) ↔ (adj‘(𝑆𝑇)) = ((adj𝑇) ∘ (adj𝑆)))