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 30215
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 29321 . 2 class HrmOp
2 vx . . . . . . . 8 setvar 𝑥
32cv 1538 . . . . . . 7 class 𝑥
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1538 . . . . . . . 8 class 𝑦
6 vt . . . . . . . . 9 setvar 𝑡
76cv 1538 . . . . . . . 8 class 𝑡
85, 7cfv 6437 . . . . . . 7 class (𝑡𝑦)
9 csp 29293 . . . . . . 7 class ·ih
103, 8, 9co 7284 . . . . . 6 class (𝑥 ·ih (𝑡𝑦))
113, 7cfv 6437 . . . . . . 7 class (𝑡𝑥)
1211, 5, 9co 7284 . . . . . 6 class ((𝑡𝑥) ·ih 𝑦)
1310, 12wceq 1539 . . . . 5 wff (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
14 chba 29290 . . . . 5 class
1513, 4, 14wral 3065 . . . 4 wff 𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
1615, 2, 14wral 3065 . . 3 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)
17 cmap 8624 . . . 4 class m
1814, 14, 17co 7284 . . 3 class ( ℋ ↑m ℋ)
1916, 6, 18crab 3069 . 2 class {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
201, 19wceq 1539 1 wff HrmOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡𝑦)) = ((𝑡𝑥) ·ih 𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  elhmop  30244
  Copyright terms: Public domain W3C validator