# Metamath Proof Explorer

## Theorem elhmop

Description: Property defining a Hermitian Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion elhmop ${⊢}{T}\in \mathrm{HrmOp}↔\left({T}:ℋ⟶ℋ\wedge \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)$

### Proof

Step Hyp Ref Expression
1 fveq1 ${⊢}{t}={T}\to {t}\left({y}\right)={T}\left({y}\right)$
2 1 oveq2d ${⊢}{t}={T}\to {x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)$
3 fveq1 ${⊢}{t}={T}\to {t}\left({x}\right)={T}\left({x}\right)$
4 3 oveq1d ${⊢}{t}={T}\to {t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
5 2 4 eqeq12d ${⊢}{t}={T}\to \left({x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
6 5 2ralbidv ${⊢}{t}={T}\to \left(\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}↔\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)$
7 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\}$
8 6 7 elrab2 ${⊢}{T}\in \mathrm{HrmOp}↔\left({T}\in \left({ℋ}^{ℋ}\right)\wedge \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)$
9 ax-hilex ${⊢}ℋ\in \mathrm{V}$
10 9 9 elmap ${⊢}{T}\in \left({ℋ}^{ℋ}\right)↔{T}:ℋ⟶ℋ$
11 10 anbi1i ${⊢}\left({T}\in \left({ℋ}^{ℋ}\right)\wedge \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)↔\left({T}:ℋ⟶ℋ\wedge \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)$
12 8 11 bitri ${⊢}{T}\in \mathrm{HrmOp}↔\left({T}:ℋ⟶ℋ\wedge \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)$