# Metamath Proof Explorer

Description: The adjoint function equals its converse. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion cnvadj ${⊢}{{adj}_{h}}^{-1}={adj}_{h}$

### Proof

Step Hyp Ref Expression
1 cnvopab ${⊢}{\left\{⟨{u},{t}⟩|\left({u}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \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)\right\}}^{-1}=\left\{⟨{t},{u}⟩|\left({u}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \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)\right\}$
2 3ancoma ${⊢}\left({u}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \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)↔\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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 ffvelrn ${⊢}\left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to {u}\left({y}\right)\in ℋ$
4 ax-his1 ${⊢}\left({u}\left({y}\right)\in ℋ\wedge {x}\in ℋ\right)\to {u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}=\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)}$
5 3 4 sylan ${⊢}\left(\left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\wedge {x}\in ℋ\right)\to {u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}=\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)}$
6 5 adantrl ${⊢}\left(\left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\wedge \left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\right)\to {u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}=\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)}$
7 ffvelrn ${⊢}\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {t}\left({x}\right)\in ℋ$
8 ax-his1 ${⊢}\left({y}\in ℋ\wedge {t}\left({x}\right)\in ℋ\right)\to {y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)=\stackrel{‾}{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}}$
9 7 8 sylan2 ${⊢}\left({y}\in ℋ\wedge \left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\right)\to {y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)=\stackrel{‾}{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}}$
10 9 adantll ${⊢}\left(\left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\wedge \left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\right)\to {y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)=\stackrel{‾}{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}}$
11 6 10 eqeq12d ${⊢}\left(\left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\wedge \left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\right)\to \left({u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)↔\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)}=\stackrel{‾}{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}}\right)$
12 11 ancoms ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge \left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\right)\to \left({u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)↔\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)}=\stackrel{‾}{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}}\right)$
13 hicl ${⊢}\left({x}\in ℋ\wedge {u}\left({y}\right)\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\in ℂ$
14 3 13 sylan2 ${⊢}\left({x}\in ℋ\wedge \left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\in ℂ$
15 14 adantll ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge \left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\right)\to {x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\in ℂ$
16 hicl ${⊢}\left({t}\left({x}\right)\in ℋ\wedge {y}\in ℋ\right)\to {t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ$
17 7 16 sylan ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\to {t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ$
18 17 adantrl ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge \left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\right)\to {t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ$
19 cj11 ${⊢}\left({x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)\in ℂ\wedge {t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\in ℂ\right)\to \left(\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)}=\stackrel{‾}{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}}↔{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
20 15 18 19 syl2anc ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge \left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\right)\to \left(\stackrel{‾}{{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)}=\stackrel{‾}{{t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}}↔{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
21 12 20 bitr2d ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\wedge \left({u}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\right)\to \left({x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)\right)$
22 21 an4s ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)\right)$
23 22 anassrs ${⊢}\left(\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)\right)$
24 eqcom ${⊢}{u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}={y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)↔{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}$
25 23 24 syl6bb ${⊢}\left(\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
26 25 ralbidva ${⊢}\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
27 26 ralbidva ${⊢}\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}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
28 ralcom ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}$
29 27 28 syl6bb ${⊢}\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}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
30 29 pm5.32i ${⊢}\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}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)↔\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
31 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}}{u}\left({y}\right)={t}\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}}{u}\left({y}\right)={t}\left({x}\right){\cdot }_{\mathrm{ih}}{y}\right)$
32 df-3an ${⊢}\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)↔\left(\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\right)\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
33 30 31 32 3bitr4i ${⊢}\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \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)↔\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
34 2 33 bitri ${⊢}\left({u}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \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)↔\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)$
35 34 opabbii ${⊢}\left\{⟨{t},{u}⟩|\left({u}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \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)\right\}=\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)\right\}$
36 1 35 eqtri ${⊢}{\left\{⟨{u},{t}⟩|\left({u}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \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)\right\}}^{-1}=\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)\right\}$
37 dfadj2 ${⊢}{adj}_{h}=\left\{⟨{u},{t}⟩|\left({u}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \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)\right\}$
38 37 cnveqi ${⊢}{{adj}_{h}}^{-1}={\left\{⟨{u},{t}⟩|\left({u}:ℋ⟶ℋ\wedge {t}:ℋ⟶ℋ\wedge \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)\right\}}^{-1}$
39 dfadj2 ${⊢}{adj}_{h}=\left\{⟨{t},{u}⟩|\left({t}:ℋ⟶ℋ\wedge {u}:ℋ⟶ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{y}{\cdot }_{\mathrm{ih}}{t}\left({x}\right)={u}\left({y}\right){\cdot }_{\mathrm{ih}}{x}\right)\right\}$
40 36 38 39 3eqtr4i ${⊢}{{adj}_{h}}^{-1}={adj}_{h}$