# Metamath Proof Explorer

Description: A property that determines the adjoint of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjeq ${⊢}\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)\to {adj}_{h}\left({T}\right)={S}$

### Proof

Step Hyp Ref Expression
1 funadj ${⊢}\mathrm{Fun}{adj}_{h}$
2 df-adjh ${⊢}{adj}_{h}=\left\{⟨{z},{w}⟩|\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{z}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)\right\}$
3 2 eleq2i ${⊢}⟨{T},{S}⟩\in {adj}_{h}↔⟨{T},{S}⟩\in \left\{⟨{z},{w}⟩|\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{z}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)\right\}$
4 ax-hilex ${⊢}ℋ\in \mathrm{V}$
5 fex ${⊢}\left({T}:ℋ⟶ℋ\wedge ℋ\in \mathrm{V}\right)\to {T}\in \mathrm{V}$
6 4 5 mpan2 ${⊢}{T}:ℋ⟶ℋ\to {T}\in \mathrm{V}$
7 fex ${⊢}\left({S}:ℋ⟶ℋ\wedge ℋ\in \mathrm{V}\right)\to {S}\in \mathrm{V}$
8 4 7 mpan2 ${⊢}{S}:ℋ⟶ℋ\to {S}\in \mathrm{V}$
9 feq1 ${⊢}{z}={T}\to \left({z}:ℋ⟶ℋ↔{T}:ℋ⟶ℋ\right)$
10 fveq1 ${⊢}{z}={T}\to {z}\left({x}\right)={T}\left({x}\right)$
11 10 oveq1d ${⊢}{z}={T}\to {z}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
12 11 eqeq1d ${⊢}{z}={T}\to \left({z}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)↔{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)$
13 12 2ralbidv ${⊢}{z}={T}\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{z}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)$
14 9 13 3anbi13d ${⊢}{z}={T}\to \left(\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{z}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)↔\left({T}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)\right)$
15 feq1 ${⊢}{w}={S}\to \left({w}:ℋ⟶ℋ↔{S}:ℋ⟶ℋ\right)$
16 fveq1 ${⊢}{w}={S}\to {w}\left({y}\right)={S}\left({y}\right)$
17 16 oveq2d ${⊢}{w}={S}\to {x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)$
18 17 eqeq2d ${⊢}{w}={S}\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)↔{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)$
19 18 2ralbidv ${⊢}{w}={S}\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)$
20 15 19 3anbi23d ${⊢}{w}={S}\to \left(\left({T}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)↔\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)\right)$
21 14 20 opelopabg ${⊢}\left({T}\in \mathrm{V}\wedge {S}\in \mathrm{V}\right)\to \left(⟨{T},{S}⟩\in \left\{⟨{z},{w}⟩|\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{z}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)\right\}↔\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)\right)$
22 6 8 21 syl2an ${⊢}\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\to \left(⟨{T},{S}⟩\in \left\{⟨{z},{w}⟩|\left({z}:ℋ⟶ℋ\wedge {w}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{z}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{w}\left({y}\right)\right)\right\}↔\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)\right)$
23 3 22 syl5bb ${⊢}\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\to \left(⟨{T},{S}⟩\in {adj}_{h}↔\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)\right)$
24 df-3an ${⊢}\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)↔\left(\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)$
25 24 baibr ${⊢}\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)↔\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)\right)$
26 23 25 bitr4d ${⊢}\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\right)\to \left(⟨{T},{S}⟩\in {adj}_{h}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)$
27 26 biimp3ar ${⊢}\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)\to ⟨{T},{S}⟩\in {adj}_{h}$
28 funopfv ${⊢}\mathrm{Fun}{adj}_{h}\to \left(⟨{T},{S}⟩\in {adj}_{h}\to {adj}_{h}\left({T}\right)={S}\right)$
29 1 27 28 mpsyl ${⊢}\left({T}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{S}\left({y}\right)\right)\to {adj}_{h}\left({T}\right)={S}$