# Metamath Proof Explorer

## 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({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{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 ${setvar}{t}$
2 chba ${class}ℋ$
3 cmap ${class}{↑}_{𝑚}$
4 2 2 3 co ${class}\left({ℋ}^{ℋ}\right)$
5 vx ${setvar}{x}$
6 vy ${setvar}{y}$
7 5 cv ${setvar}{x}$
8 csp ${class}{\cdot }_{\mathrm{ih}}$
9 1 cv ${setvar}{t}$
10 6 cv ${setvar}{y}$
11 10 9 cfv ${class}{t}\left({y}\right)$
12 7 11 8 co ${class}\left({x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)\right)$
13 7 9 cfv ${class}{t}\left({x}\right)$
14 13 10 8 co ${class}\left({t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
15 12 14 wceq ${wff}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
16 15 6 2 wral ${wff}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{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 ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{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({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{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({ℋ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right\}$