# Metamath Proof Explorer

## Theorem unop

Description: Basic inner product property of a unitary operator. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 elunop ${⊢}{T}\in \mathrm{UniOp}↔\left({T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{y}\right)$
2 1 simprbi ${⊢}{T}\in \mathrm{UniOp}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
3 2 3ad2ant1 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
4 fveq2 ${⊢}{x}={A}\to {T}\left({x}\right)={T}\left({A}\right)$
5 4 oveq1d ${⊢}{x}={A}\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)$
6 oveq1 ${⊢}{x}={A}\to {x}{\cdot }_{\mathrm{ih}}{y}={A}{\cdot }_{\mathrm{ih}}{y}$
7 5 6 eqeq12d ${⊢}{x}={A}\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{y}↔{T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={A}{\cdot }_{\mathrm{ih}}{y}\right)$
8 fveq2 ${⊢}{y}={B}\to {T}\left({y}\right)={T}\left({B}\right)$
9 8 oveq2d ${⊢}{y}={B}\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)$
10 oveq2 ${⊢}{y}={B}\to {A}{\cdot }_{\mathrm{ih}}{y}={A}{\cdot }_{\mathrm{ih}}{B}$
11 9 10 eqeq12d ${⊢}{y}={B}\to \left({T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={A}{\cdot }_{\mathrm{ih}}{y}↔{T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\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}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{y}\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{B}\right)$
13 12 3adant1 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{y}\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{B}\right)$
14 3 13 mpd ${⊢}\left({T}\in \mathrm{UniOp}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {T}\left({A}\right){\cdot }_{\mathrm{ih}}{T}\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{B}$