# Metamath Proof Explorer

## Theorem hmoval

Description: The set of Hermitian (self-adjoint) operators on a normed complex vector space. (Contributed by NM, 26-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses hmoval.8 ${⊢}{H}=\mathrm{HmOp}\left({U}\right)$
hmoval.9 ${⊢}{A}={U}\mathrm{adj}{U}$
Assertion hmoval ${⊢}{U}\in \mathrm{NrmCVec}\to {H}=\left\{{t}\in \mathrm{dom}{A}|{A}\left({t}\right)={t}\right\}$

### Proof

Step Hyp Ref Expression
1 hmoval.8 ${⊢}{H}=\mathrm{HmOp}\left({U}\right)$
2 hmoval.9 ${⊢}{A}={U}\mathrm{adj}{U}$
3 oveq12 ${⊢}\left({u}={U}\wedge {u}={U}\right)\to {u}\mathrm{adj}{u}={U}\mathrm{adj}{U}$
4 3 anidms ${⊢}{u}={U}\to {u}\mathrm{adj}{u}={U}\mathrm{adj}{U}$
5 4 2 syl6eqr ${⊢}{u}={U}\to {u}\mathrm{adj}{u}={A}$
6 5 dmeqd ${⊢}{u}={U}\to \mathrm{dom}\left({u}\mathrm{adj}{u}\right)=\mathrm{dom}{A}$
7 5 fveq1d ${⊢}{u}={U}\to \left({u}\mathrm{adj}{u}\right)\left({t}\right)={A}\left({t}\right)$
8 7 eqeq1d ${⊢}{u}={U}\to \left(\left({u}\mathrm{adj}{u}\right)\left({t}\right)={t}↔{A}\left({t}\right)={t}\right)$
9 6 8 rabeqbidv ${⊢}{u}={U}\to \left\{{t}\in \mathrm{dom}\left({u}\mathrm{adj}{u}\right)|\left({u}\mathrm{adj}{u}\right)\left({t}\right)={t}\right\}=\left\{{t}\in \mathrm{dom}{A}|{A}\left({t}\right)={t}\right\}$
10 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)$
11 ovex ${⊢}{U}\mathrm{adj}{U}\in \mathrm{V}$
12 2 11 eqeltri ${⊢}{A}\in \mathrm{V}$
13 12 dmex ${⊢}\mathrm{dom}{A}\in \mathrm{V}$
14 13 rabex ${⊢}\left\{{t}\in \mathrm{dom}{A}|{A}\left({t}\right)={t}\right\}\in \mathrm{V}$
15 9 10 14 fvmpt ${⊢}{U}\in \mathrm{NrmCVec}\to \mathrm{HmOp}\left({U}\right)=\left\{{t}\in \mathrm{dom}{A}|{A}\left({t}\right)={t}\right\}$
16 1 15 syl5eq ${⊢}{U}\in \mathrm{NrmCVec}\to {H}=\left\{{t}\in \mathrm{dom}{A}|{A}\left({t}\right)={t}\right\}$