Theorem curf2val

Description: Value of a component of the curry functor natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	curf2.g	$$⊢G=⟨C,D⟩{curry}_{F}F$$
	curf2.a	$$⊢A={\mathrm{Base}}_C$$
	curf2.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	curf2.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	curf2.f	$$⊢\phi \to F\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}E\right)$$
	curf2.b	$$⊢B={\mathrm{Base}}_D$$
	curf2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	curf2.i	$$⊢I=\mathrm{Id}\left(D\right)$$
	curf2.x	$$⊢\phi \to X\in A$$
	curf2.y	$$⊢\phi \to Y\in A$$
	curf2.k	$$⊢\phi \to K\in \left(XHY\right)$$
	curf2.l	$$⊢L=\left(X{2}^{nd}\left(G\right)Y\right)\left(K\right)$$
	curf2.z	$$⊢\phi \to Z\in B$$
Assertion	curf2val	$$⊢\phi \to L\left(Z\right)=K\left(⟨X,Z⟩2^{nd}\left(F\right)⟨Y,Z⟩\right)I\left(Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		curf2.g	$$⊢G=⟨C,D⟩{curry}_{F}F$$
2		curf2.a	$$⊢A={\mathrm{Base}}_C$$
3		curf2.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		curf2.d	$$⊢\phi \to D\in \mathrm{Cat}$$
5		curf2.f	$$⊢\phi \to F\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}E\right)$$
6		curf2.b	$$⊢B={\mathrm{Base}}_D$$
7		curf2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
8		curf2.i	$$⊢I=\mathrm{Id}\left(D\right)$$
9		curf2.x	$$⊢\phi \to X\in A$$
10		curf2.y	$$⊢\phi \to Y\in A$$
11		curf2.k	$$⊢\phi \to K\in \left(XHY\right)$$
12		curf2.l	$$⊢L=\left(X{2}^{nd}\left(G\right)Y\right)\left(K\right)$$
13		curf2.z	$$⊢\phi \to Z\in B$$
14	1 2 3 4 5 6 7 8 9 10 11 12	curf2	$$⊢\phi \to L=\left(z\in B⟼K\left(⟨X,z⟩2^{nd}\left(F\right)⟨Y,z⟩\right)I\left(z\right)\right)$$
15		simpr	$$⊢\left(\phi \wedge z=Z\right)\to z=Z$$
16	15	opeq2d	$$⊢\left(\phi \wedge z=Z\right)\to ⟨X,z⟩=⟨X,Z⟩$$
17	15	opeq2d	$$⊢\left(\phi \wedge z=Z\right)\to ⟨Y,z⟩=⟨Y,Z⟩$$
18	16 17	oveq12d	$$⊢\left(\phi \wedge z=Z\right)\to ⟨X,z⟩2^{nd}\left(F\right)⟨Y,z⟩=⟨X,Z⟩2^{nd}\left(F\right)⟨Y,Z⟩$$
19		eqidd	$$⊢\left(\phi \wedge z=Z\right)\to K=K$$
20	15	fveq2d	$$⊢\left(\phi \wedge z=Z\right)\to I\left(z\right)=I\left(Z\right)$$
21	18 19 20	oveq123d	$$⊢\left(\phi \wedge z=Z\right)\to K\left(⟨X,z⟩2^{nd}\left(F\right)⟨Y,z⟩\right)I\left(z\right)=K\left(⟨X,Z⟩2^{nd}\left(F\right)⟨Y,Z⟩\right)I\left(Z\right)$$
22		ovexd	$$⊢\phi \to K\left(⟨X,Z⟩2^{nd}\left(F\right)⟨Y,Z⟩\right)I\left(Z\right)\in \mathrm{V}$$
23	14 21 13 22	fvmptd	$$⊢\phi \to L\left(Z\right)=K\left(⟨X,Z⟩2^{nd}\left(F\right)⟨Y,Z⟩\right)I\left(Z\right)$$