Metamath Proof Explorer

Definition df-hmo

Description: Define the set of Hermitian (self-adjoint) operators on a normed complex vector space (normally a Hilbert space). Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

Ref Expression
Assertion df-hmo ⊢ HmOp = u ∈ NrmCVec ⟼ t ∈ dom ⁡ u adj u | u adj u ⁡ t = t

Detailed syntax breakdown

Step Hyp Ref Expression
0 chmo class HmOp
1 vu setvar u
2 cnv class NrmCVec
3 vt setvar t
4 1 cv setvar u
5 caj class adj
6 4 4 5 co class u adj u
7 6 cdm class dom ⁡ u adj u
8 3 cv setvar t
9 8 6 cfv class u adj u ⁡ t
10 9 8 wceq wff u adj u ⁡ t = t
11 10 3 7 crab class t ∈ dom ⁡ u adj u | u adj u ⁡ t = t
12 1 2 11 cmpt class u ∈ NrmCVec ⟼ t ∈ dom ⁡ u adj u | u adj u ⁡ t = t
13 0 12 wceq wff HmOp = u ∈ NrmCVec ⟼ t ∈ dom ⁡ u adj u | u adj u ⁡ t = t