Definition df-hmop

Description: Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators", sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hmop	$$⊢\mathrm{HrmOp}=\left\{t\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=t\left(x\right){\cdot }_{\mathrm{ih}}y\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cho	$$class\mathrm{HrmOp}$$
1		vt	$$setvart$$
2		chba	$$class\mathscr{H}$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4	2 2 3	co	$$class\left({\mathscr{H}}^{\mathscr{H}}\right)$$
5		vx	$$setvarx$$
6		vy	$$setvary$$
7	5	cv	$$setvarx$$
8		csp	$$class{\cdot }_{\mathrm{ih}}$$
9	1	cv	$$setvart$$
10	6	cv	$$setvary$$
11	10 9	cfv	$$classt\left(y\right)$$
12	7 11 8	co	$$class\left(x{\cdot }_{\mathrm{ih}}t\left(y\right)\right)$$
13	7 9	cfv	$$classt\left(x\right)$$
14	13 10 8	co	$$class\left(t\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
15	12 14	wceq	$$wffx{\cdot }_{\mathrm{ih}}t\left(y\right)=t\left(x\right){\cdot }_{\mathrm{ih}}y$$
16	15 6 2	wral	$$wff\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=t\left(x\right){\cdot }_{\mathrm{ih}}y$$
17	16 5 2	wral	$$wff\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=t\left(x\right){\cdot }_{\mathrm{ih}}y$$
18	17 1 4	crab	$$class\left\{t\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=t\left(x\right){\cdot }_{\mathrm{ih}}y\right\}$$
19	0 18	wceq	$$wff\mathrm{HrmOp}=\left\{t\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=t\left(x\right){\cdot }_{\mathrm{ih}}y\right\}$$