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

Definition df-hmop 28687
 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 = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
Distinct variable group:   𝑥,𝑡,𝑦

Detailed syntax breakdown of Definition df-hmop
StepHypRef Expression
1 cho 27791 . 2 class HrmOp
2 vx . . . . . . . 8 setvar 𝑥
32cv 1481 . . . . . . 7 class 𝑥
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1481 . . . . . . . 8 class 𝑦
6 vt . . . . . . . . 9 setvar 𝑡
76cv 1481 . . . . . . . 8 class 𝑡
85, 7cfv 5886 . . . . . . 7 class (𝑡𝑦)
9 csp 27763 . . . . . . 7 class ·ih
103, 8, 9co 6647 . . . . . 6 class (𝑥 ·ih (𝑡𝑦))
113, 7cfv 5886 . . . . . . 7 class (𝑡𝑥)
1211, 5, 9co 6647 . . . . . 6 class ((𝑡𝑥) ·ih 𝑦)
1310, 12wceq 1482 . . . . 5 wff (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
14 chil 27760 . . . . 5 class
1513, 4, 14wral 2911 . . . 4 wff 𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
1615, 2, 14wral 2911 . . 3 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
17 cmap 7854 . . . 4 class 𝑚
1814, 14, 17co 6647 . . 3 class ( ℋ ↑𝑚 ℋ)
1916, 6, 18crab 2915 . 2 class {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
201, 19wceq 1482 1 wff HrmOp = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
 Colors of variables: wff setvar class This definition is referenced by:  elhmop  28716
 Copyright terms: Public domain W3C validator