Theorem funadj

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:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right\}\leftrightarrow \forall t{\exists }^{*}u\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
2		adjmo	$$⊢{\exists }^{*}u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
3		3simpc	$$⊢\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\to \left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
4	3	moimi	$$⊢{\exists }^{*}u\left(u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)\to {\exists }^{*}u\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
5	2 4	ax-mp	$$⊢{\exists }^{*}u\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}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:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}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:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}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\leftrightarrow \mathrm{Fun}\left\{⟨t,u⟩|\left(t:\mathscr{H}⟶\mathscr{H}\wedge u:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}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$$