# Metamath Proof Explorer

## Theorem ishmo

Description: The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 hmoval.8 ${⊢}{H}=\mathrm{HmOp}\left({U}\right)$
2 hmoval.9 ${⊢}{A}={U}\mathrm{adj}{U}$
3 1 2 hmoval ${⊢}{U}\in \mathrm{NrmCVec}\to {H}=\left\{{t}\in \mathrm{dom}{A}|{A}\left({t}\right)={t}\right\}$
4 3 eleq2d ${⊢}{U}\in \mathrm{NrmCVec}\to \left({T}\in {H}↔{T}\in \left\{{t}\in \mathrm{dom}{A}|{A}\left({t}\right)={t}\right\}\right)$
5 fveq2 ${⊢}{t}={T}\to {A}\left({t}\right)={A}\left({T}\right)$
6 id ${⊢}{t}={T}\to {t}={T}$
7 5 6 eqeq12d ${⊢}{t}={T}\to \left({A}\left({t}\right)={t}↔{A}\left({T}\right)={T}\right)$
8 7 elrab ${⊢}{T}\in \left\{{t}\in \mathrm{dom}{A}|{A}\left({t}\right)={t}\right\}↔\left({T}\in \mathrm{dom}{A}\wedge {A}\left({T}\right)={T}\right)$
9 4 8 syl6bb ${⊢}{U}\in \mathrm{NrmCVec}\to \left({T}\in {H}↔\left({T}\in \mathrm{dom}{A}\wedge {A}\left({T}\right)={T}\right)\right)$