Definition df-hmo 28832

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 28830	. 2 class HmOp
2		vu	. . 3 setvar 𝑢
3		cnv 28665	. . 3 class NrmCVec
4		vt	. . . . . . 7 setvar 𝑡
5	4	cv 1542	. . . . . 6 class 𝑡
6	2	cv 1542	. . . . . . 7 class 𝑢
7		caj 28829	. . . . . . 7 class adj
8	6, 6, 7	co 7213	. . . . . 6 class (𝑢adj𝑢)
9	5, 8	cfv 6380	. . . . 5 class ((𝑢adj𝑢)‘𝑡)
10	9, 5	wceq 1543	. . . 4 wff ((𝑢adj𝑢)‘𝑡) = 𝑡
11	8	cdm 5551	. . . 4 class dom (𝑢adj𝑢)
12	10, 4, 11	crab 3065	. . 3 class {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡}
13	2, 3, 12	cmpt 5135	. 2 class (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡})
14	1, 13	wceq 1543	1 wff HmOp = (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡})

This definition is referenced by:  hmoval  28891