Metamath Proof Explorer

Definition df-hmop

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.)

Ref Expression
Assertion df-hmop ⊢ HrmOp = t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cho class HrmOp
1 vt setvar t
2 chba class ℋ
3 cmap class ↑ 𝑚
4 2 2 3 co class ℋ ℋ
5 vx setvar x
6 vy setvar y
7 5 cv setvar x
8 csp class ⋅ ih
9 1 cv setvar t
10 6 cv setvar y
11 10 9 cfv class t ⁡ y
12 7 11 8 co class x ⋅ ih t ⁡ y
13 7 9 cfv class t ⁡ x
14 13 10 8 co class t ⁡ x ⋅ ih y
15 12 14 wceq wff x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y
16 15 6 2 wral wff ∀ y ∈ ℋ x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y
17 16 5 2 wral wff ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y
18 17 1 4 crab class t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y
19 0 18 wceq wff HrmOp = t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = t ⁡ x ⋅ ih y