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

 Description: The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression

Dummy variables 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bdopadj 29773 . . . 4 (𝑇 ∈ BndLinOp → 𝑇 ∈ dom adj)
2 adjval 29581 . . . 4 (𝑇 ∈ dom adj → (adj𝑇) = (𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)))
31, 2syl 17 . . 3 (𝑇 ∈ BndLinOp → (adj𝑇) = (𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)))
4 cnlnadj 29770 . . . . . 6 (𝑇 ∈ (LinOp ∩ ContOp) → ∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦)))
5 lncnopbd 29728 . . . . . 6 (𝑇 ∈ (LinOp ∩ ContOp) ↔ 𝑇 ∈ BndLinOp)
6 lncnbd 29729 . . . . . . 7 (LinOp ∩ ContOp) = BndLinOp
76rexeqi 3420 . . . . . 6 (∃𝑡 ∈ (LinOp ∩ ContOp)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦)) ↔ ∃𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦)))
84, 5, 73imtr3i 292 . . . . 5 (𝑇 ∈ BndLinOp → ∃𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦)))
9 bdopf 29553 . . . . . . . 8 (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶ ℋ)
10 bdopf 29553 . . . . . . . 8 (𝑡 ∈ BndLinOp → 𝑡: ℋ⟶ ℋ)
11 adjsym 29524 . . . . . . . 8 ((𝑇: ℋ⟶ ℋ ∧ 𝑡: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑇𝑥) ·ih 𝑦)))
129, 10, 11syl2an 595 . . . . . . 7 ((𝑇 ∈ BndLinOp ∧ 𝑡 ∈ BndLinOp) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑇𝑥) ·ih 𝑦)))
13 eqcom 2833 . . . . . . . 8 (((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦)) ↔ (𝑥 ·ih (𝑡𝑦)) = ((𝑇𝑥) ·ih 𝑦))
14132ralbii 3171 . . . . . . 7 (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦)) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑇𝑥) ·ih 𝑦))
1512, 14syl6bbr 290 . . . . . 6 ((𝑇 ∈ BndLinOp ∧ 𝑡 ∈ BndLinOp) → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦))))
1615rexbidva 3301 . . . . 5 (𝑇 ∈ BndLinOp → (∃𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) ↔ ∃𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑇𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑡𝑦))))
178, 16mpbird 258 . . . 4 (𝑇 ∈ BndLinOp → ∃𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦))
18 adjeu 29580 . . . . . 6 (𝑇: ℋ⟶ ℋ → (𝑇 ∈ dom adj ↔ ∃!𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)))
199, 18syl 17 . . . . 5 (𝑇 ∈ BndLinOp → (𝑇 ∈ dom adj ↔ ∃!𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)))
201, 19mpbid 233 . . . 4 (𝑇 ∈ BndLinOp → ∃!𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦))
21 ax-hilex 28690 . . . . . . . 8 ℋ ∈ V
2221, 21elmap 8425 . . . . . . 7 (𝑡 ∈ ( ℋ ↑m ℋ) ↔ 𝑡: ℋ⟶ ℋ)
2310, 22sylibr 235 . . . . . 6 (𝑡 ∈ BndLinOp → 𝑡 ∈ ( ℋ ↑m ℋ))
2423ssriv 3975 . . . . 5 BndLinOp ⊆ ( ℋ ↑m ℋ)
25 id 22 . . . . . 6 (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦))
2625rgenw 3155 . . . . 5 𝑡 ∈ BndLinOp (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦))
27 riotass2 7136 . . . . 5 (((BndLinOp ⊆ ( ℋ ↑m ℋ) ∧ ∀𝑡 ∈ BndLinOp (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) → ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦))) ∧ (∃𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) ∧ ∃!𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦))) → (𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)) = (𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)))
2824, 26, 27mpanl12 698 . . . 4 ((∃𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) ∧ ∃!𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)) → (𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)) = (𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)))
2917, 20, 28syl2anc 584 . . 3 (𝑇 ∈ BndLinOp → (𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)) = (𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)))
303, 29eqtr4d 2864 . 2 (𝑇 ∈ BndLinOp → (adj𝑇) = (𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)))
3124a1i 11 . . . 4 (𝑇 ∈ BndLinOp → BndLinOp ⊆ ( ℋ ↑m ℋ))
32 reuss 4288 . . . 4 ((BndLinOp ⊆ ( ℋ ↑m ℋ) ∧ ∃𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) ∧ ∃!𝑡 ∈ ( ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)) → ∃!𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦))
3331, 17, 20, 32syl3anc 1365 . . 3 (𝑇 ∈ BndLinOp → ∃!𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦))
34 riotacl 7123 . . 3 (∃!𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦) → (𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)) ∈ BndLinOp)
3533, 34syl 17 . 2 (𝑇 ∈ BndLinOp → (𝑡 ∈ BndLinOp ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇𝑦)) = ((𝑡𝑥) ·ih 𝑦)) ∈ BndLinOp)
3630, 35eqeltrd 2918 1 (𝑇 ∈ BndLinOp → (adj𝑇) ∈ BndLinOp)