Theorem diag2

Description: Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017)

	Ref	Expression
Hypotheses	diag2.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	diag2.a	$$⊢A={\mathrm{Base}}_C$$
	diag2.b	$$⊢B={\mathrm{Base}}_D$$
	diag2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	diag2.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	diag2.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	diag2.x	$$⊢\phi \to X\in A$$
	diag2.y	$$⊢\phi \to Y\in A$$
	diag2.f	$$⊢\phi \to F\in \left(XHY\right)$$
Assertion	diag2	$$⊢\phi \to \left(X{2}^{nd}\left(L\right)Y\right)\left(F\right)=B\times \left\{F\right\}$$

Proof

Step	Hyp	Ref	Expression
1		diag2.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		diag2.a	$$⊢A={\mathrm{Base}}_C$$
3		diag2.b	$$⊢B={\mathrm{Base}}_D$$
4		diag2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		diag2.c	$$⊢\phi \to C\in \mathrm{Cat}$$
6		diag2.d	$$⊢\phi \to D\in \mathrm{Cat}$$
7		diag2.x	$$⊢\phi \to X\in A$$
8		diag2.y	$$⊢\phi \to Y\in A$$
9		diag2.f	$$⊢\phi \to F\in \left(XHY\right)$$
10	1 5 6	diagval	$$⊢\phi \to L=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$
11	10	fveq2d	$$⊢\phi \to 2^{nd}\left(L\right)=2^{nd}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)$$
12	11	oveqd	$$⊢\phi \to X{2}^{nd}\left(L\right)Y=X{2}^{nd}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)Y$$
13	12	fveq1d	$$⊢\phi \to \left(X{2}^{nd}\left(L\right)Y\right)\left(F\right)=\left(X{2}^{nd}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)Y\right)\left(F\right)$$
14		eqid	$$⊢⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$
15		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
16		eqid	$$⊢C{1^{st}}_{F}D=C{1^{st}}_{F}D$$
17	15 5 6 16	1stfcl	$$⊢\phi \to C{1^{st}}_{F}D\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}C\right)$$
18		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
19		eqid	$$⊢\left(X{2}^{nd}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)Y\right)\left(F\right)=\left(X{2}^{nd}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)Y\right)\left(F\right)$$
20	14 2 5 6 17 3 4 18 7 8 9 19	curf2	$$⊢\phi \to \left(X{2}^{nd}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)Y\right)\left(F\right)=\left(x\in B⟼F\left(⟨X,x⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨Y,x⟩\right)\mathrm{Id}\left(D\right)\left(x\right)\right)$$
21	15 2 3	xpcbas	$$⊢A\times B={\mathrm{Base}}_{\left(C{\times }_{c}D\right)}$$
22		eqid	$$⊢\mathrm{Hom}\left(C{\times }_{c}D\right)=\mathrm{Hom}\left(C{\times }_{c}D\right)$$
23	5	adantr	$$⊢\left(\phi \wedge x\in B\right)\to C\in \mathrm{Cat}$$
24	6	adantr	$$⊢\left(\phi \wedge x\in B\right)\to D\in \mathrm{Cat}$$
25		opelxpi	$$⊢\left(X\in A\wedge x\in B\right)\to ⟨X,x⟩\in \left(A\times B\right)$$
26	7 25	sylan	$$⊢\left(\phi \wedge x\in B\right)\to ⟨X,x⟩\in \left(A\times B\right)$$
27		opelxpi	$$⊢\left(Y\in A\wedge x\in B\right)\to ⟨Y,x⟩\in \left(A\times B\right)$$
28	8 27	sylan	$$⊢\left(\phi \wedge x\in B\right)\to ⟨Y,x⟩\in \left(A\times B\right)$$
29	15 21 22 23 24 16 26 28	1stf2	$$⊢\left(\phi \wedge x\in B\right)\to ⟨X,x⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨Y,x⟩={1^{st}\upharpoonright }_{\left(⟨X,x⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Y,x⟩\right)}$$
30	29	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to F\left(⟨X,x⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨Y,x⟩\right)\mathrm{Id}\left(D\right)\left(x\right)=F\left({1^{st}\upharpoonright }_{\left(⟨X,x⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Y,x⟩\right)}\right)\mathrm{Id}\left(D\right)\left(x\right)$$
31		df-ov	$$⊢F\left({1^{st}\upharpoonright }_{\left(⟨X,x⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Y,x⟩\right)}\right)\mathrm{Id}\left(D\right)\left(x\right)=\left({1^{st}\upharpoonright }_{\left(⟨X,x⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Y,x⟩\right)}\right)\left(⟨F,\mathrm{Id}\left(D\right)\left(x\right)⟩\right)$$
32	9	adantr	$$⊢\left(\phi \wedge x\in B\right)\to F\in \left(XHY\right)$$
33		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
34		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
35	3 33 18 24 34	catidcl	$$⊢\left(\phi \wedge x\in B\right)\to \mathrm{Id}\left(D\right)\left(x\right)\in \left(x\mathrm{Hom}\left(D\right)x\right)$$
36	32 35	opelxpd	$$⊢\left(\phi \wedge x\in B\right)\to ⟨F,\mathrm{Id}\left(D\right)\left(x\right)⟩\in \left(\left(XHY\right)\times \left(x\mathrm{Hom}\left(D\right)x\right)\right)$$
37	7	adantr	$$⊢\left(\phi \wedge x\in B\right)\to X\in A$$
38	8	adantr	$$⊢\left(\phi \wedge x\in B\right)\to Y\in A$$
39	15 2 3 4 33 37 34 38 34 22	xpchom2	$$⊢\left(\phi \wedge x\in B\right)\to ⟨X,x⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Y,x⟩=\left(XHY\right)\times \left(x\mathrm{Hom}\left(D\right)x\right)$$
40	36 39	eleqtrrd	$$⊢\left(\phi \wedge x\in B\right)\to ⟨F,\mathrm{Id}\left(D\right)\left(x\right)⟩\in \left(⟨X,x⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Y,x⟩\right)$$
41	40	fvresd	$$⊢\left(\phi \wedge x\in B\right)\to \left({1^{st}\upharpoonright }_{\left(⟨X,x⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Y,x⟩\right)}\right)\left(⟨F,\mathrm{Id}\left(D\right)\left(x\right)⟩\right)=1^{st}\left(⟨F,\mathrm{Id}\left(D\right)\left(x\right)⟩\right)$$
42	31 41	syl5eq	$$⊢\left(\phi \wedge x\in B\right)\to F\left({1^{st}\upharpoonright }_{\left(⟨X,x⟩\mathrm{Hom}\left(C{\times }_{c}D\right)⟨Y,x⟩\right)}\right)\mathrm{Id}\left(D\right)\left(x\right)=1^{st}\left(⟨F,\mathrm{Id}\left(D\right)\left(x\right)⟩\right)$$
43		op1stg	$$⊢\left(F\in \left(XHY\right)\wedge \mathrm{Id}\left(D\right)\left(x\right)\in \left(x\mathrm{Hom}\left(D\right)x\right)\right)\to 1^{st}\left(⟨F,\mathrm{Id}\left(D\right)\left(x\right)⟩\right)=F$$
44	9 35 43	syl2an2r	$$⊢\left(\phi \wedge x\in B\right)\to 1^{st}\left(⟨F,\mathrm{Id}\left(D\right)\left(x\right)⟩\right)=F$$
45	30 42 44	3eqtrd	$$⊢\left(\phi \wedge x\in B\right)\to F\left(⟨X,x⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨Y,x⟩\right)\mathrm{Id}\left(D\right)\left(x\right)=F$$
46	45	mpteq2dva	$$⊢\phi \to \left(x\in B⟼F\left(⟨X,x⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨Y,x⟩\right)\mathrm{Id}\left(D\right)\left(x\right)\right)=\left(x\in B⟼F\right)$$
47		fconstmpt	$$⊢B\times \left\{F\right\}=\left(x\in B⟼F\right)$$
48	46 47	eqtr4di	$$⊢\phi \to \left(x\in B⟼F\left(⟨X,x⟩2^{nd}\left(C{1^{st}}_{F}D\right)⟨Y,x⟩\right)\mathrm{Id}\left(D\right)\left(x\right)\right)=B\times \left\{F\right\}$$
49	13 20 48	3eqtrd	$$⊢\phi \to \left(X{2}^{nd}\left(L\right)Y\right)\left(F\right)=B\times \left\{F\right\}$$