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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chmo	|- HmOp
1		vu	|- u
2		cnv	|- NrmCVec
3		vt	|- t
4	1	cv	|- u
5		caj	|- adj
6	4 4 5	co	|- ( u adj u )
7	6	cdm	|- dom ( u adj u )
8	3	cv	|- t
9	8 6	cfv	|- ( ( u adj u ) ` t )
10	9 8	wceq	|- ( ( u adj u ) ` t ) = t
11	10 3 7	crab	|- { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t }
12	1 2 11	cmpt	|- ( u e. NrmCVec |-> { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t } )
13	0 12	wceq	|- HmOp = ( u e. NrmCVec |-> { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t } )