Definition df-hmop 29615

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

Step	Hyp	Ref	Expression
1		cho 28721	. 2 class HrmOp
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1532	. . . . . . 7 class 𝑥
4		vy	. . . . . . . . 9 setvar 𝑦
5	4	cv 1532	. . . . . . . 8 class 𝑦
6		vt	. . . . . . . . 9 setvar 𝑡
7	6	cv 1532	. . . . . . . 8 class 𝑡
8	5, 7	cfv 6349	. . . . . . 7 class (𝑡‘𝑦)
9		csp 28693	. . . . . . 7 class ·ih
10	3, 8, 9	co 7150	. . . . . 6 class (𝑥 ·ih (𝑡‘𝑦))
11	3, 7	cfv 6349	. . . . . . 7 class (𝑡‘𝑥)
12	11, 5, 9	co 7150	. . . . . 6 class ((𝑡‘𝑥) ·ih 𝑦)
13	10, 12	wceq 1533	. . . . 5 wff (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)
14		chba 28690	. . . . 5 class ℋ
15	13, 4, 14	wral 3138	. . . 4 wff ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)
16	15, 2, 14	wral 3138	. . 3 wff ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)
17		cmap 8400	. . . 4 class ↑m
18	14, 14, 17	co 7150	. . 3 class ( ℋ ↑m ℋ)
19	16, 6, 18	crab 3142	. 2 class {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)}
20	1, 19	wceq 1533	1 wff HrmOp = {𝑡 ∈ ( ℋ ↑m ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑡‘𝑥) ·ih 𝑦)}

This definition is referenced by:  elhmop  29644