# Metamath Proof Explorer

## 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 ${setvar}{u}$
2 cnv ${class}\mathrm{NrmCVec}$
3 vt ${setvar}{t}$
4 1 cv ${setvar}{u}$
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 ${setvar}{t}$
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)$