Theorem adjval

Description: Value of the adjoint function for T in the domain of adjh . (Contributed by NM, 19-Feb-2006) (Revised by Mario Carneiro, 24-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	adjval	$$⊢T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right)=\left(\iota u\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\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)$$

Proof

Step	Hyp	Ref	Expression
1		dmadjop	$$⊢T\in \mathrm{dom}{adj}_h\to T:\mathscr{H}⟶\mathscr{H}$$
2	1	biantrurd	$$⊢T\in \mathrm{dom}{adj}_h\to \left(\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)\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \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)\right)\right)$$
3		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
4	3 3	elmap	$$⊢u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\leftrightarrow u:\mathscr{H}⟶\mathscr{H}$$
5	4	anbi1i	$$⊢\left(u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\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)\leftrightarrow \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)$$
6		3anass	$$⊢\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)\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \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)\right)$$
7	2 5 6	3bitr4g	$$⊢T\in \mathrm{dom}{adj}_h\to \left(\left(u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\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)\leftrightarrow \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	iotabidv	$$⊢T\in \mathrm{dom}{adj}_h\to \left(\iota u|\left(u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\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)=\left(\iota 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		df-riota	$$⊢\left(\iota u\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\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)=\left(\iota u|\left(u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\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)$$
10	9	a1i	$$⊢T\in \mathrm{dom}{adj}_h\to \left(\iota u\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\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)=\left(\iota u|\left(u\in \left({\mathscr{H}}^{\mathscr{H}}\right)\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)$$
11		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\}$$
12		feq1	$$⊢t=T\to \left(t:\mathscr{H}⟶\mathscr{H}\leftrightarrow T:\mathscr{H}⟶\mathscr{H}\right)$$
13		fveq1	$$⊢t=T\to t\left(y\right)=T\left(y\right)$$
14	13	oveq2d	$$⊢t=T\to x{\cdot }_{\mathrm{ih}}t\left(y\right)=x{\cdot }_{\mathrm{ih}}T\left(y\right)$$
15	14	eqeq1d	$$⊢t=T\to \left(x{\cdot }_{\mathrm{ih}}t\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\leftrightarrow x{\cdot }_{\mathrm{ih}}T\left(y\right)=u\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
16	15	2ralbidv	$$⊢t=T\to \left(\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\leftrightarrow \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)$$
17	12 16	3anbi13d	$$⊢t=T\to \left(\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)\leftrightarrow \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)$$
18	11 17	fvopab5	$$⊢T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right)=\left(\iota 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)$$
19	8 10 18	3eqtr4rd	$$⊢T\in \mathrm{dom}{adj}_h\to {adj}_h\left(T\right)=\left(\iota u\in \left({\mathscr{H}}^{\mathscr{H}}\right)|\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)$$