Definition df-hmo 27606

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 = ( u e. NrmCVec |-> { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t } )

Distinct variable group:   u, t

Detailed syntax breakdown of Definition df-hmo

Step	Hyp	Ref	Expression
1		chmo 27604	. 2 class HmOp
2		vu	. . 3 setvar u
3		cnv 27439	. . 3 class NrmCVec
4		vt	. . . . . . 7 setvar t
5	4	cv 1482	. . . . . 6 class t
6	2	cv 1482	. . . . . . 7 class u
7		caj 27603	. . . . . . 7 class adj
8	6, 6, 7	co 6650	. . . . . 6 class ( u adj u )
9	5, 8	cfv 5888	. . . . 5 class ( ( u adj u ) ` t )
10	9, 5	wceq 1483	. . . 4 wff ( ( u adj u ) ` t ) = t
11	8	cdm 5114	. . . 4 class dom ( u adj u )
12	10, 4, 11	crab 2916	. . 3 class { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t }
13	2, 3, 12	cmpt 4729	. 2 class ( u e. NrmCVec |-> { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t } )
14	1, 13	wceq 1483	1 wff HmOp = ( u e. NrmCVec |-> { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t } )

This definition is referenced by:  hmoval  27665