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 27880
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 28114) 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 26984 . 2 class adj
2 chil 26948 . . . . 5 class
3 vt . . . . . 6 setvar 𝑡
43cv 1473 . . . . 5 class 𝑡
52, 2, 4wf 5685 . . . 4 wff 𝑡: ℋ⟶ ℋ
6 vu . . . . . 6 setvar 𝑢
76cv 1473 . . . . 5 class 𝑢
82, 2, 7wf 5685 . . . 4 wff 𝑢: ℋ⟶ ℋ
9 vx . . . . . . . . . 10 setvar 𝑥
109cv 1473 . . . . . . . . 9 class 𝑥
1110, 4cfv 5689 . . . . . . . 8 class (𝑡𝑥)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1473 . . . . . . . 8 class 𝑦
14 csp 26951 . . . . . . . 8 class ·ih
1511, 13, 14co 6426 . . . . . . 7 class ((𝑡𝑥) ·ih 𝑦)
1613, 7cfv 5689 . . . . . . . 8 class (𝑢𝑦)
1710, 16, 14co 6426 . . . . . . 7 class (𝑥 ·ih (𝑢𝑦))
1815, 17wceq 1474 . . . . . 6 wff ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
1918, 12, 2wral 2800 . . . . 5 wff 𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
2019, 9, 2wral 2800 . . . 4 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦))
215, 8, 20w3a 1030 . . 3 wff (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))
2221, 3, 6copab 4540 . 2 class {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))}
231, 22wceq 1474 1 wff adj = {⟨𝑡, 𝑢⟩ ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((𝑡𝑥) ·ih 𝑦) = (𝑥 ·ih (𝑢𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  dfadj2  27916  adjeq  27966
  Copyright terms: Public domain W3C validator