Theorem diag12

Description: Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	diagval.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	diagval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	diagval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	diag11.a	$$⊢A={\mathrm{Base}}_C$$
	diag11.c	$$⊢\phi \to X\in A$$
	diag11.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
	diag11.b	$$⊢B={\mathrm{Base}}_D$$
	diag11.y	$$⊢\phi \to Y\in B$$
	diag12.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	diag12.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	diag12.z	$$⊢\phi \to Z\in B$$
	diag12.f	$$⊢\phi \to F\in \left(YJZ\right)$$
Assertion	diag12	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Z\right)\left(F\right)=\underset{\dot{}}{1}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		diagval.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		diagval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		diagval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
4		diag11.a	$$⊢A={\mathrm{Base}}_C$$
5		diag11.c	$$⊢\phi \to X\in A$$
6		diag11.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
7		diag11.b	$$⊢B={\mathrm{Base}}_D$$
8		diag11.y	$$⊢\phi \to Y\in B$$
9		diag12.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
10		diag12.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
11		diag12.z	$$⊢\phi \to Z\in B$$
12		diag12.f	$$⊢\phi \to F\in \left(YJZ\right)$$
13	1 2 3	diagval	$$⊢\phi \to L=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$
14	13	fveq2d	$$⊢\phi \to 1^{st}\left(L\right)=1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)$$
15	14	fveq1d	$$⊢\phi \to 1^{st}\left(L\right)\left(X\right)=1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)$$
16	6 15	syl5eq	$$⊢\phi \to K=1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)$$
17	16	fveq2d	$$⊢\phi \to 2^{nd}\left(K\right)=2^{nd}\left(1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)\right)$$
18	17	oveqd	$$⊢\phi \to Y{2}^{nd}\left(K\right)Z=Y{2}^{nd}\left(1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)\right)Z$$
19	18	fveq1d	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Z\right)\left(F\right)=\left(Y{2}^{nd}\left(1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)\right)Z\right)\left(F\right)$$
20		eqid	$$⊢⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$
21		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
22		eqid	$$⊢C{1^{st}}_{F}D=C{1^{st}}_{F}D$$
23	21 2 3 22	1stfcl	$$⊢\phi \to C{1^{st}}_{F}D\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}C\right)$$
24		eqid	$$⊢1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)=1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)$$
25	20 4 2 3 23 7 5 24 8 9 10 11 12	curf12	$$⊢\phi \to \left(Y{2}^{nd}\left(1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)\right)Z\right)\left(F\right)=\underset{\dot{}}{1}\left(X\right)\left(⟨X,Y⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨X,Z⟩\right)F$$
26		df-ov	$$⊢\underset{\dot{}}{1}\left(X\right)\left(⟨X,Y⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨X,Z⟩\right)F=\left(⟨X,Y⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨X,Z⟩\right)\left(⟨\underset{\dot{}}{1}\left(X\right),F⟩\right)$$
27	21 4 7	xpcbas	$$⊢A\times B={\mathrm{Base}}_{\left(C{\times }_{c}D\right)}$$
28		eqid	$$⊢\mathrm{Hom}\left(C{\times }_{c}D\right)=\mathrm{Hom}\left(C{\times }_{c}D\right)$$
29	5 8	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left(A\times B\right)$$
30	5 11	opelxpd	$$⊢\phi \to ⟨X,Z⟩\in \left(A\times B\right)$$
31	21 27 28 2 3 22 29 30	1stf2	$$⊢\phi \to ⟨X,Y⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨X,Z⟩={1^{st}\upharpoonright }_{\left(⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨X,Z⟩\right)}$$
32	31	fveq1d	$$⊢\phi \to \left(⟨X,Y⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨X,Z⟩\right)\left(⟨\underset{\dot{}}{1}\left(X\right),F⟩\right)=\left({1^{st}\upharpoonright }_{\left(⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨X,Z⟩\right)}\right)\left(⟨\underset{\dot{}}{1}\left(X\right),F⟩\right)$$
33	26 32	syl5eq	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\left(⟨X,Y⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨X,Z⟩\right)F=\left({1^{st}\upharpoonright }_{\left(⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨X,Z⟩\right)}\right)\left(⟨\underset{\dot{}}{1}\left(X\right),F⟩\right)$$
34		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
35	4 34 10 2 5	catidcl	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)$$
36	35 12	opelxpd	$$⊢\phi \to ⟨\underset{\dot{}}{1}\left(X\right),F⟩\in \left(\left(X\mathrm{Hom}\left(C\right)X\right)\times \left(YJZ\right)\right)$$
37	21 4 7 34 9 5 8 5 11 28	xpchom2	$$⊢\phi \to ⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨X,Z⟩=\left(X\mathrm{Hom}\left(C\right)X\right)\times \left(YJZ\right)$$
38	36 37	eleqtrrd	$$⊢\phi \to ⟨\underset{\dot{}}{1}\left(X\right),F⟩\in \left(⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨X,Z⟩\right)$$
39	38	fvresd	$$⊢\phi \to \left({1^{st}\upharpoonright }_{\left(⟨X,Y⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨X,Z⟩\right)}\right)\left(⟨\underset{\dot{}}{1}\left(X\right),F⟩\right)=1^{st}\left(⟨\underset{\dot{}}{1}\left(X\right),F⟩\right)$$
40		op1stg	$$⊢\left(\underset{\dot{}}{1}\left(X\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)\wedge F\in \left(YJZ\right)\right)\to 1^{st}\left(⟨\underset{\dot{}}{1}\left(X\right),F⟩\right)=\underset{\dot{}}{1}\left(X\right)$$
41	35 12 40	syl2anc	$$⊢\phi \to 1^{st}\left(⟨\underset{\dot{}}{1}\left(X\right),F⟩\right)=\underset{\dot{}}{1}\left(X\right)$$
42	33 39 41	3eqtrd	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\left(⟨X,Y⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨X,Z⟩\right)F=\underset{\dot{}}{1}\left(X\right)$$
43	19 25 42	3eqtrd	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Z\right)\left(F\right)=\underset{\dot{}}{1}\left(X\right)$$