# Metamath Proof Explorer

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

Ref Expression
Assertion dfadj2 ${⊢}{adj}_{h}=\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 df-adjh ${⊢}{adj}_{h}=\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\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}}{u}\left({y}\right)\right)\right\}$
2 adjsym ${⊢}\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\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)={u}\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}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
3 eqcom ${⊢}{t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)↔{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
4 3 2ralbii ${⊢}\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}}{u}\left({y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}$
5 2 4 syl6rbbr ${⊢}\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\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}}{u}\left({y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
6 5 pm5.32i ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\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}}{u}\left({y}\right)\right)↔\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
7 df-3an ${⊢}\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\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}}{u}\left({y}\right)\right)↔\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\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}}{u}\left({y}\right)\right)$
8 df-3an ${⊢}\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)↔\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
9 6 7 8 3bitr4i ${⊢}\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\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}}{u}\left({y}\right)\right)↔\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
10 9 opabbii ${⊢}\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\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}}{u}\left({y}\right)\right)\right\}=\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right\}$
11 1 10 eqtri ${⊢}{adj}_{h}=\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)={u}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)\right\}$