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

Definition df-hmop 29636
 Description: Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators", sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-hmop HrmOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
Distinct variable group:   𝑥,𝑡,𝑦

Detailed syntax breakdown of Definition df-hmop
StepHypRef Expression
1 cho 28742 . 2 class HrmOp
2 vx . . . . . . . 8 setvar 𝑥
32cv 1537 . . . . . . 7 class 𝑥
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1537 . . . . . . . 8 class 𝑦
6 vt . . . . . . . . 9 setvar 𝑡
76cv 1537 . . . . . . . 8 class 𝑡
85, 7cfv 6345 . . . . . . 7 class (𝑡𝑦)
9 csp 28714 . . . . . . 7 class ·ih
103, 8, 9co 7151 . . . . . 6 class (𝑥 ·ih (𝑡𝑦))
113, 7cfv 6345 . . . . . . 7 class (𝑡𝑥)
1211, 5, 9co 7151 . . . . . 6 class ((𝑡𝑥) ·ih 𝑦)
1310, 12wceq 1538 . . . . 5 wff (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
14 chba 28711 . . . . 5 class
1513, 4, 14wral 3133 . . . 4 wff 𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
1615, 2, 14wral 3133 . . 3 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
17 cmap 8404 . . . 4 class m
1814, 14, 17co 7151 . . 3 class ( ℋ ↑m ℋ)
1916, 6, 18crab 3137 . 2 class {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
201, 19wceq 1538 1 wff HrmOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
 Colors of variables: wff setvar class This definition is referenced by:  elhmop  29665
 Copyright terms: Public domain W3C validator