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

Definition df-adjh 28092
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 28326) 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 27196 . 2 class adj
2 chil 27160 . . . . 5 class
3 vt . . . . . 6 setvar 𝑡
43cv 1474 . . . . 5 class 𝑡
52, 2, 4wf 5800 . . . 4 wff 𝑡: ℋ⟶ ℋ
6 vu . . . . . 6 setvar 𝑢
76cv 1474 . . . . 5 class 𝑢
82, 2, 7wf 5800 . . . 4 wff 𝑢: ℋ⟶ ℋ
9 vx . . . . . . . . . 10 setvar 𝑥
109cv 1474 . . . . . . . . 9 class 𝑥
1110, 4cfv 5804 . . . . . . . 8 class (𝑡𝑥)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1474 . . . . . . . 8 class 𝑦
14 csp 27163 . . . . . . . 8 class ·ih
1511, 13, 14co 6549 . . . . . . 7 class ((𝑡𝑥) ·ih 𝑦)
1613, 7cfv 5804 . . . . . . . 8 class (𝑢𝑦)
1710, 16, 14co 6549 . . . . . . 7 class (𝑥 ·ih (𝑢𝑦))
1815, 17wceq 1475 . . . . . 6 wff ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
1918, 12, 2wral 2896 . . . . 5 wff 𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
2019, 9, 2wral 2896 . . . 4 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
215, 8, 20w3a 1031 . . 3 wff (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))
2221, 3, 6copab 4642 . 2 class {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))}
231, 22wceq 1475 1 wff adj = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  dfadj2  28128  adjeq  28178
  Copyright terms: Public domain W3C validator