# Metamath Proof Explorer

## Theorem adj1

Description: Property of an adjoint Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 funadj ${⊢}\mathrm{Fun}{adj}_{h}$
2 funfvop ${⊢}\left(\mathrm{Fun}{adj}_{h}\wedge {T}\in \mathrm{dom}{adj}_{h}\right)\to ⟨{T},{adj}_{h}\left({T}\right)⟩\in {adj}_{h}$
3 1 2 mpan ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to ⟨{T},{adj}_{h}\left({T}\right)⟩\in {adj}_{h}$
4 dfadj2 ${⊢}{adj}_{h}=\left\{⟨{z},{w}⟩|\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{z}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right\}$
5 3 4 eleqtrdi ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to ⟨{T},{adj}_{h}\left({T}\right)⟩\in \left\{⟨{z},{w}⟩|\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{z}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right\}$
6 fvex ${⊢}{adj}_{h}\left({T}\right)\in \mathrm{V}$
7 feq1 ${⊢}{z}={T}\to \left({z}:ℋ⟶ℋ↔{T}:ℋ⟶ℋ\right)$
8 fveq1 ${⊢}{z}={T}\to {z}\left({y}\right)={T}\left({y}\right)$
9 8 oveq2d ${⊢}{z}={T}\to {x}{\cdot }_{\mathrm{ih}}{z}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)$
10 9 eqeq1d ${⊢}{z}={T}\to \left({x}{\cdot }_{\mathrm{ih}}{z}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
11 10 2ralbidv ${⊢}{z}={T}\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{z}\left({y}\right)={w}\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)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
12 7 11 3anbi13d ${⊢}{z}={T}\to \left(\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{z}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)↔\left({T}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)$
13 feq1 ${⊢}{w}={adj}_{h}\left({T}\right)\to \left({w}:ℋ⟶ℋ↔{adj}_{h}\left({T}\right):ℋ⟶ℋ\right)$
14 fveq1 ${⊢}{w}={adj}_{h}\left({T}\right)\to {w}\left({x}\right)={adj}_{h}\left({T}\right)\left({x}\right)$
15 14 oveq1d ${⊢}{w}={adj}_{h}\left({T}\right)\to {w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
16 15 eqeq2d ${⊢}{w}={adj}_{h}\left({T}\right)\to \left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
17 16 2ralbidv ${⊢}{w}={adj}_{h}\left({T}\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)={w}\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)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
18 13 17 3anbi23d ${⊢}{w}={adj}_{h}\left({T}\right)\to \left(\left({T}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)↔\left({T}:ℋ⟶ℋ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)$
19 12 18 opelopabg ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {adj}_{h}\left({T}\right)\in \mathrm{V}\right)\to \left(⟨{T},{adj}_{h}\left({T}\right)⟩\in \left\{⟨{z},{w}⟩|\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{z}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right\}↔\left({T}:ℋ⟶ℋ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)$
20 6 19 mpan2 ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left(⟨{T},{adj}_{h}\left({T}\right)⟩\in \left\{⟨{z},{w}⟩|\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{z}\left({y}\right)={w}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right\}↔\left({T}:ℋ⟶ℋ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right)$
21 5 20 mpbid ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left({T}:ℋ⟶ℋ\wedge {adj}_{h}\left({T}\right):ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
22 21 simp3d ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
23 oveq1 ${⊢}{x}={A}\to {x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={A}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)$
24 fveq2 ${⊢}{x}={A}\to {adj}_{h}\left({T}\right)\left({x}\right)={adj}_{h}\left({T}\right)\left({A}\right)$
25 24 oveq1d ${⊢}{x}={A}\to {adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}={adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{y}$
26 23 25 eqeq12d ${⊢}{x}={A}\to \left({x}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{A}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{y}\right)$
27 fveq2 ${⊢}{y}={B}\to {T}\left({y}\right)={T}\left({B}\right)$
28 27 oveq2d ${⊢}{y}={B}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)$
29 oveq2 ${⊢}{y}={B}\to {adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{y}={adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{B}$
30 28 29 eqeq12d ${⊢}{y}={B}\to \left({A}{\cdot }_{\mathrm{ih}}{T}\left({y}\right)={adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{y}↔{A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{B}\right)$
31 26 30 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)={adj}_{h}\left({T}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{y}\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{B}\right)$
32 22 31 syl5com ${⊢}{T}\in \mathrm{dom}{adj}_{h}\to \left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{B}\right)$
33 32 3impib ${⊢}\left({T}\in \mathrm{dom}{adj}_{h}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{T}\left({B}\right)={adj}_{h}\left({T}\right)\left({A}\right){\cdot }_{\mathrm{ih}}{B}$