Metamath Proof Explorer

Description: Functionality of the adjoint function. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion funadj ${⊢}\mathrm{Fun}{adj}_{h}$

Proof

Step Hyp Ref Expression
1 funopab ${⊢}\mathrm{Fun}\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\}↔\forall {t}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{u}\phantom{\rule{.4em}{0ex}}\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)$
2 adjmo ${⊢}{\exists }^{*}{u}\phantom{\rule{.4em}{0ex}}\left({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)$
3 3simpc ${⊢}\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)\to \left({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)$
4 3 moimi ${⊢}{\exists }^{*}{u}\phantom{\rule{.4em}{0ex}}\left({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)\to {\exists }^{*}{u}\phantom{\rule{.4em}{0ex}}\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)$
5 2 4 ax-mp ${⊢}{\exists }^{*}{u}\phantom{\rule{.4em}{0ex}}\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)$
6 1 5 mpgbir ${⊢}\mathrm{Fun}\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\}$
7 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\}$
8 7 funeqi ${⊢}\mathrm{Fun}{adj}_{h}↔\mathrm{Fun}\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\}$
9 6 8 mpbir ${⊢}\mathrm{Fun}{adj}_{h}$