# Metamath Proof Explorer

## Theorem hmop

Description: Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmop ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}$

### Proof

Step Hyp Ref Expression
1 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)$
2 1 simprbi ${⊢}{T}\in \mathrm{HrmOp}\to \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}$
3 2 3ad2ant1 ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to \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}$
4 oveq1 ${⊢}{x}={A}\to {x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={A}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)$
5 fveq2 ${⊢}{x}={A}\to {T}\left({x}\right)={T}\left({A}\right)$
6 5 oveq1d ${⊢}{x}={A}\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({A}\right){\cdot }_{\mathrm{ih}}{y}$
7 4 6 eqeq12d ${⊢}{x}={A}\to \left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{A}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{y}\right)$
8 fveq2 ${⊢}{y}={B}\to {T}\left({y}\right)={T}\left({B}\right)$
9 8 oveq2d ${⊢}{y}={B}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)$
10 oveq2 ${⊢}{y}={B}\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}$
11 9 10 eqeq12d ${⊢}{y}={B}\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{y}↔{A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}\right)$
12 7 11 rspc2v ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\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}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}\right)$
13 12 3adant1 ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\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}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}\right)$
14 3 13 mpd ${⊢}\left({T}\in \mathrm{HrmOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{B}$