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

Definition df-adjh 29630
 Description: Define the adjoint of a Hilbert space operator (if it exists). The domain of adjℎ is the set of all adjoint operators. Definition of adjoint in [Kalmbach2] p. 8. Unlike Kalmbach (and most authors), we do not demand that the operator be linear, but instead show (in adjbdln 29864) that the adjoint exists for a bounded linear operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-adjh adj = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))}
Distinct variable group:   𝑢,𝑡,𝑥,𝑦

Detailed syntax breakdown of Definition df-adjh
StepHypRef Expression
1 cado 28736 . 2 class adj
2 chba 28700 . . . . 5 class
3 vt . . . . . 6 setvar 𝑡
43cv 1537 . . . . 5 class 𝑡
52, 2, 4wf 6340 . . . 4 wff 𝑡: ℋ⟶ ℋ
6 vu . . . . . 6 setvar 𝑢
76cv 1537 . . . . 5 class 𝑢
82, 2, 7wf 6340 . . . 4 wff 𝑢: ℋ⟶ ℋ
9 vx . . . . . . . . . 10 setvar 𝑥
109cv 1537 . . . . . . . . 9 class 𝑥
1110, 4cfv 6344 . . . . . . . 8 class (𝑡𝑥)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1537 . . . . . . . 8 class 𝑦
14 csp 28703 . . . . . . . 8 class ·ih
1511, 13, 14co 7146 . . . . . . 7 class ((𝑡𝑥) ·ih 𝑦)
1613, 7cfv 6344 . . . . . . . 8 class (𝑢𝑦)
1710, 16, 14co 7146 . . . . . . 7 class (𝑥 ·ih (𝑢𝑦))
1815, 17wceq 1538 . . . . . 6 wff ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
1918, 12, 2wral 3133 . . . . 5 wff 𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
2019, 9, 2wral 3133 . . . 4 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
215, 8, 20w3a 1084 . . 3 wff (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))
2221, 3, 6copab 5115 . 2 class {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))}
231, 22wceq 1538 1 wff adj = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))}
 Colors of variables: wff setvar class This definition is referenced by:  dfadj2  29666  adjeq  29716
 Copyright terms: Public domain W3C validator