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	$$⊢\mathrm{HmOp}=\left(u\in \mathrm{NrmCVec}⟼\left\{t\in \mathrm{dom}\left(u\mathrm{adj}u\right)|\left(u\mathrm{adj}u\right)\left(t\right)=t\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chmo	$$class\mathrm{HmOp}$$
1		vu	$$setvaru$$
2		cnv	$$class\mathrm{NrmCVec}$$
3		vt	$$setvart$$
4	1	cv	$$setvaru$$
5		caj	$$class\mathrm{adj}$$
6	4 4 5	co	$$class\left(u\mathrm{adj}u\right)$$
7	6	cdm	$$class\mathrm{dom}\left(u\mathrm{adj}u\right)$$
8	3	cv	$$setvart$$
9	8 6	cfv	$$class\left(u\mathrm{adj}u\right)\left(t\right)$$
10	9 8	wceq	$$wff\left(u\mathrm{adj}u\right)\left(t\right)=t$$
11	10 3 7	crab	$$class\left\{t\in \mathrm{dom}\left(u\mathrm{adj}u\right)|\left(u\mathrm{adj}u\right)\left(t\right)=t\right\}$$
12	1 2 11	cmpt	$$class\left(u\in \mathrm{NrmCVec}⟼\left\{t\in \mathrm{dom}\left(u\mathrm{adj}u\right)|\left(u\mathrm{adj}u\right)\left(t\right)=t\right\}\right)$$
13	0 12	wceq	$$wff\mathrm{HmOp}=\left(u\in \mathrm{NrmCVec}⟼\left\{t\in \mathrm{dom}\left(u\mathrm{adj}u\right)|\left(u\mathrm{adj}u\right)\left(t\right)=t\right\}\right)$$