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

Definition df-hmop 29043
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 28147 . 2 class HrmOp
2 vx . . . . . . . 8 setvar 𝑥
32cv 1630 . . . . . . 7 class 𝑥
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1630 . . . . . . . 8 class 𝑦
6 vt . . . . . . . . 9 setvar 𝑡
76cv 1630 . . . . . . . 8 class 𝑡
85, 7cfv 6031 . . . . . . 7 class (𝑡𝑦)
9 csp 28119 . . . . . . 7 class ·ih
103, 8, 9co 6793 . . . . . 6 class (𝑥 ·ih (𝑡𝑦))
113, 7cfv 6031 . . . . . . 7 class (𝑡𝑥)
1211, 5, 9co 6793 . . . . . 6 class ((𝑡𝑥) ·ih 𝑦)
1310, 12wceq 1631 . . . . 5 wff (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
14 chil 28116 . . . . 5 class
1513, 4, 14wral 3061 . . . 4 wff 𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
1615, 2, 14wral 3061 . . 3 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
17 cmap 8009 . . . 4 class 𝑚
1814, 14, 17co 6793 . . 3 class ( ℋ ↑𝑚 ℋ)
1916, 6, 18crab 3065 . 2 class {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
201, 19wceq 1631 1 wff HrmOp = {𝑡 ∈ ( ℋ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  elhmop  29072
  Copyright terms: Public domain W3C validator