Definition df-hmo 30770

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

Assertion

Ref	Expression
df-hmo	⊢ HmOp = (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡})

Distinct variable group:   𝑢,𝑡

Detailed syntax breakdown of Definition df-hmo

Step	Hyp	Ref	Expression
1		chmo 30768	. 2 class HmOp
2		vu	. . 3 setvar 𝑢
3		cnv 30603	. . 3 class NrmCVec
4		vt	. . . . . . 7 setvar 𝑡
5	4	cv 1539	. . . . . 6 class 𝑡
6	2	cv 1539	. . . . . . 7 class 𝑢
7		caj 30767	. . . . . . 7 class adj
8	6, 6, 7	co 7431	. . . . . 6 class (𝑢adj𝑢)
9	5, 8	cfv 6561	. . . . 5 class ((𝑢adj𝑢)‘𝑡)
10	9, 5	wceq 1540	. . . 4 wff ((𝑢adj𝑢)‘𝑡) = 𝑡
11	8	cdm 5685	. . . 4 class dom (𝑢adj𝑢)
12	10, 4, 11	crab 3436	. . 3 class {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡}
13	2, 3, 12	cmpt 5225	. 2 class (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡})
14	1, 13	wceq 1540	1 wff HmOp = (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡})

This definition is referenced by:  hmoval  30829