Theorem xpcco2

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpcco2.t	$$⊢T=C{\times }_{c}D$$
	xpcco2.x	$$⊢X={\mathrm{Base}}_C$$
	xpcco2.y	$$⊢Y={\mathrm{Base}}_D$$
	xpcco2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	xpcco2.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	xpcco2.m	$$⊢\phi \to M\in X$$
	xpcco2.n	$$⊢\phi \to N\in Y$$
	xpcco2.p	$$⊢\phi \to P\in X$$
	xpcco2.q	$$⊢\phi \to Q\in Y$$
	xpcco2.o1	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	xpcco2.o2	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(D\right)$$
	xpcco2.o	$$⊢O=\mathrm{comp}\left(T\right)$$
	xpcco2.r	$$⊢\phi \to R\in X$$
	xpcco2.s	$$⊢\phi \to S\in Y$$
	xpcco2.f	$$⊢\phi \to F\in \left(MHP\right)$$
	xpcco2.g	$$⊢\phi \to G\in \left(NJQ\right)$$
	xpcco2.k	$$⊢\phi \to K\in \left(PHR\right)$$
	xpcco2.l	$$⊢\phi \to L\in \left(QJS\right)$$
Assertion	xpcco2	$$⊢\phi \to ⟨K,L⟩\left(⟨⟨M,N⟩,⟨P,Q⟩⟩O⟨R,S⟩\right)⟨F,G⟩=⟨K\left(⟨M,P⟩\underset{\dot{}}{·}R\right)F,L\left(⟨N,Q⟩\underset{\dot{}}{\bullet }S\right)G⟩$$

Proof

Step	Hyp	Ref	Expression
1		xpcco2.t	$$⊢T=C{\times }_{c}D$$
2		xpcco2.x	$$⊢X={\mathrm{Base}}_C$$
3		xpcco2.y	$$⊢Y={\mathrm{Base}}_D$$
4		xpcco2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		xpcco2.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
6		xpcco2.m	$$⊢\phi \to M\in X$$
7		xpcco2.n	$$⊢\phi \to N\in Y$$
8		xpcco2.p	$$⊢\phi \to P\in X$$
9		xpcco2.q	$$⊢\phi \to Q\in Y$$
10		xpcco2.o1	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
11		xpcco2.o2	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(D\right)$$
12		xpcco2.o	$$⊢O=\mathrm{comp}\left(T\right)$$
13		xpcco2.r	$$⊢\phi \to R\in X$$
14		xpcco2.s	$$⊢\phi \to S\in Y$$
15		xpcco2.f	$$⊢\phi \to F\in \left(MHP\right)$$
16		xpcco2.g	$$⊢\phi \to G\in \left(NJQ\right)$$
17		xpcco2.k	$$⊢\phi \to K\in \left(PHR\right)$$
18		xpcco2.l	$$⊢\phi \to L\in \left(QJS\right)$$
19	1 2 3	xpcbas	$$⊢X\times Y={\mathrm{Base}}_T$$
20		eqid	$$⊢\mathrm{Hom}\left(T\right)=\mathrm{Hom}\left(T\right)$$
21	6 7	opelxpd	$$⊢\phi \to ⟨M,N⟩\in \left(X\times Y\right)$$
22	8 9	opelxpd	$$⊢\phi \to ⟨P,Q⟩\in \left(X\times Y\right)$$
23	13 14	opelxpd	$$⊢\phi \to ⟨R,S⟩\in \left(X\times Y\right)$$
24	15 16	opelxpd	$$⊢\phi \to ⟨F,G⟩\in \left(\left(MHP\right)\times \left(NJQ\right)\right)$$
25	1 2 3 4 5 6 7 8 9 20	xpchom2	$$⊢\phi \to ⟨M,N⟩\mathrm{Hom}\left(T\right)⟨P,Q⟩=\left(MHP\right)\times \left(NJQ\right)$$
26	24 25	eleqtrrd	$$⊢\phi \to ⟨F,G⟩\in \left(⟨M,N⟩\mathrm{Hom}\left(T\right)⟨P,Q⟩\right)$$
27	17 18	opelxpd	$$⊢\phi \to ⟨K,L⟩\in \left(\left(PHR\right)\times \left(QJS\right)\right)$$
28	1 2 3 4 5 8 9 13 14 20	xpchom2	$$⊢\phi \to ⟨P,Q⟩\mathrm{Hom}\left(T\right)⟨R,S⟩=\left(PHR\right)\times \left(QJS\right)$$
29	27 28	eleqtrrd	$$⊢\phi \to ⟨K,L⟩\in \left(⟨P,Q⟩\mathrm{Hom}\left(T\right)⟨R,S⟩\right)$$
30	1 19 20 10 11 12 21 22 23 26 29	xpcco	$$⊢\phi \to ⟨K,L⟩\left(⟨⟨M,N⟩,⟨P,Q⟩⟩O⟨R,S⟩\right)⟨F,G⟩=⟨1^{st}\left(⟨K,L⟩\right)\left(⟨1^{st}\left(⟨M,N⟩\right),1^{st}\left(⟨P,Q⟩\right)⟩\underset{\dot{}}{·}{1}^{st}\left(⟨R,S⟩\right)\right)1^{st}\left(⟨F,G⟩\right),2^{nd}\left(⟨K,L⟩\right)\left(⟨2^{nd}\left(⟨M,N⟩\right),2^{nd}\left(⟨P,Q⟩\right)⟩\underset{\dot{}}{\bullet }{2}^{nd}\left(⟨R,S⟩\right)\right)2^{nd}\left(⟨F,G⟩\right)⟩$$
31		op1stg	$$⊢\left(M\in X\wedge N\in Y\right)\to 1^{st}\left(⟨M,N⟩\right)=M$$
32	6 7 31	syl2anc	$$⊢\phi \to 1^{st}\left(⟨M,N⟩\right)=M$$
33		op1stg	$$⊢\left(P\in X\wedge Q\in Y\right)\to 1^{st}\left(⟨P,Q⟩\right)=P$$
34	8 9 33	syl2anc	$$⊢\phi \to 1^{st}\left(⟨P,Q⟩\right)=P$$
35	32 34	opeq12d	$$⊢\phi \to ⟨1^{st}\left(⟨M,N⟩\right),1^{st}\left(⟨P,Q⟩\right)⟩=⟨M,P⟩$$
36		op1stg	$$⊢\left(R\in X\wedge S\in Y\right)\to 1^{st}\left(⟨R,S⟩\right)=R$$
37	13 14 36	syl2anc	$$⊢\phi \to 1^{st}\left(⟨R,S⟩\right)=R$$
38	35 37	oveq12d	$$⊢\phi \to ⟨1^{st}\left(⟨M,N⟩\right),1^{st}\left(⟨P,Q⟩\right)⟩\underset{\dot{}}{·}{1}^{st}\left(⟨R,S⟩\right)=⟨M,P⟩\underset{\dot{}}{·}R$$
39		op1stg	$$⊢\left(K\in \left(PHR\right)\wedge L\in \left(QJS\right)\right)\to 1^{st}\left(⟨K,L⟩\right)=K$$
40	17 18 39	syl2anc	$$⊢\phi \to 1^{st}\left(⟨K,L⟩\right)=K$$
41		op1stg	$$⊢\left(F\in \left(MHP\right)\wedge G\in \left(NJQ\right)\right)\to 1^{st}\left(⟨F,G⟩\right)=F$$
42	15 16 41	syl2anc	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)=F$$
43	38 40 42	oveq123d	$$⊢\phi \to 1^{st}\left(⟨K,L⟩\right)\left(⟨1^{st}\left(⟨M,N⟩\right),1^{st}\left(⟨P,Q⟩\right)⟩\underset{\dot{}}{·}{1}^{st}\left(⟨R,S⟩\right)\right)1^{st}\left(⟨F,G⟩\right)=K\left(⟨M,P⟩\underset{\dot{}}{·}R\right)F$$
44		op2ndg	$$⊢\left(M\in X\wedge N\in Y\right)\to 2^{nd}\left(⟨M,N⟩\right)=N$$
45	6 7 44	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨M,N⟩\right)=N$$
46		op2ndg	$$⊢\left(P\in X\wedge Q\in Y\right)\to 2^{nd}\left(⟨P,Q⟩\right)=Q$$
47	8 9 46	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨P,Q⟩\right)=Q$$
48	45 47	opeq12d	$$⊢\phi \to ⟨2^{nd}\left(⟨M,N⟩\right),2^{nd}\left(⟨P,Q⟩\right)⟩=⟨N,Q⟩$$
49		op2ndg	$$⊢\left(R\in X\wedge S\in Y\right)\to 2^{nd}\left(⟨R,S⟩\right)=S$$
50	13 14 49	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨R,S⟩\right)=S$$
51	48 50	oveq12d	$$⊢\phi \to ⟨2^{nd}\left(⟨M,N⟩\right),2^{nd}\left(⟨P,Q⟩\right)⟩\underset{\dot{}}{\bullet }{2}^{nd}\left(⟨R,S⟩\right)=⟨N,Q⟩\underset{\dot{}}{\bullet }S$$
52		op2ndg	$$⊢\left(K\in \left(PHR\right)\wedge L\in \left(QJS\right)\right)\to 2^{nd}\left(⟨K,L⟩\right)=L$$
53	17 18 52	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨K,L⟩\right)=L$$
54		op2ndg	$$⊢\left(F\in \left(MHP\right)\wedge G\in \left(NJQ\right)\right)\to 2^{nd}\left(⟨F,G⟩\right)=G$$
55	15 16 54	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨F,G⟩\right)=G$$
56	51 53 55	oveq123d	$$⊢\phi \to 2^{nd}\left(⟨K,L⟩\right)\left(⟨2^{nd}\left(⟨M,N⟩\right),2^{nd}\left(⟨P,Q⟩\right)⟩\underset{\dot{}}{\bullet }{2}^{nd}\left(⟨R,S⟩\right)\right)2^{nd}\left(⟨F,G⟩\right)=L\left(⟨N,Q⟩\underset{\dot{}}{\bullet }S\right)G$$
57	43 56	opeq12d	$$⊢\phi \to ⟨1^{st}\left(⟨K,L⟩\right)\left(⟨1^{st}\left(⟨M,N⟩\right),1^{st}\left(⟨P,Q⟩\right)⟩\underset{\dot{}}{·}{1}^{st}\left(⟨R,S⟩\right)\right)1^{st}\left(⟨F,G⟩\right),2^{nd}\left(⟨K,L⟩\right)\left(⟨2^{nd}\left(⟨M,N⟩\right),2^{nd}\left(⟨P,Q⟩\right)⟩\underset{\dot{}}{\bullet }{2}^{nd}\left(⟨R,S⟩\right)\right)2^{nd}\left(⟨F,G⟩\right)⟩=⟨K\left(⟨M,P⟩\underset{\dot{}}{·}R\right)F,L\left(⟨N,Q⟩\underset{\dot{}}{\bullet }S\right)G⟩$$
58	30 57	eqtrd	$$⊢\phi \to ⟨K,L⟩\left(⟨⟨M,N⟩,⟨P,Q⟩⟩O⟨R,S⟩\right)⟨F,G⟩=⟨K\left(⟨M,P⟩\underset{\dot{}}{·}R\right)F,L\left(⟨N,Q⟩\underset{\dot{}}{\bullet }S\right)G⟩$$