Theorem xpcco2

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

	Ref	Expression
Hypotheses	xpcco2.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	xpcco2.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
	xpcco2.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
	xpcco2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	xpcco2.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	xpcco2.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑋 )
	xpcco2.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑌 )
	xpcco2.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
	xpcco2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑌 )
	xpcco2.o1	⊢ · = ( comp ‘ 𝐶 )
	xpcco2.o2	⊢ ∙ = ( comp ‘ 𝐷 )
	xpcco2.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
	xpcco2.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
	xpcco2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
	xpcco2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 𝐻 𝑃 ) )
	xpcco2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 𝐽 𝑄 ) )
	xpcco2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 𝐻 𝑅 ) )
	xpcco2.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑄 𝐽 𝑆 ) )
Assertion	xpcco2	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) 𝐺 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		xpcco2.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		xpcco2.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
3		xpcco2.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
4		xpcco2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		xpcco2.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
6		xpcco2.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑋 )
7		xpcco2.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑌 )
8		xpcco2.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
9		xpcco2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑌 )
10		xpcco2.o1	⊢ · = ( comp ‘ 𝐶 )
11		xpcco2.o2	⊢ ∙ = ( comp ‘ 𝐷 )
12		xpcco2.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
13		xpcco2.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
14		xpcco2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
15		xpcco2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 𝐻 𝑃 ) )
16		xpcco2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 𝐽 𝑄 ) )
17		xpcco2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 𝐻 𝑅 ) )
18		xpcco2.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑄 𝐽 𝑆 ) )
19	1 2 3	xpcbas	⊢ ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 )
20		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
21	6 7	opelxpd	⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝑋 × 𝑌 ) )
22	8 9	opelxpd	⊢ ( 𝜑 → ⟨ 𝑃 , 𝑄 ⟩ ∈ ( 𝑋 × 𝑌 ) )
23	13 14	opelxpd	⊢ ( 𝜑 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝑋 × 𝑌 ) )
24	15 16	opelxpd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑀 𝐻 𝑃 ) × ( 𝑁 𝐽 𝑄 ) ) )
25	1 2 3 4 5 6 7 8 9 20	xpchom2	⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝑁 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝑃 , 𝑄 ⟩ ) = ( ( 𝑀 𝐻 𝑃 ) × ( 𝑁 𝐽 𝑄 ) ) )
26	24 25	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ⟨ 𝑀 , 𝑁 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝑃 , 𝑄 ⟩ ) )
27	17 18	opelxpd	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( ( 𝑃 𝐻 𝑅 ) × ( 𝑄 𝐽 𝑆 ) ) )
28	1 2 3 4 5 8 9 13 14 20	xpchom2	⊢ ( 𝜑 → ( ⟨ 𝑃 , 𝑄 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝑅 , 𝑆 ⟩ ) = ( ( 𝑃 𝐻 𝑅 ) × ( 𝑄 𝐽 𝑆 ) ) )
29	27 28	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( ⟨ 𝑃 , 𝑄 ⟩ ( Hom ‘ 𝑇 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
30	1 19 20 10 11 12 21 22 23 26 29	xpcco	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ · ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ ∙ ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ⟩ )
31		op1stg	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
32	6 7 31	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
33		op1stg	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑃 )
34	8 9 33	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑃 )
35	32 34	opeq12d	⊢ ( 𝜑 → ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ = ⟨ 𝑀 , 𝑃 ⟩ )
36		op1stg	⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
37	13 14 36	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
38	35 37	oveq12d	⊢ ( 𝜑 → ( ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ · ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) = ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) )
39		op1stg	⊢ ( ( 𝐾 ∈ ( 𝑃 𝐻 𝑅 ) ∧ 𝐿 ∈ ( 𝑄 𝐽 𝑆 ) ) → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
40	17 18 39	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
41		op1stg	⊢ ( ( 𝐹 ∈ ( 𝑀 𝐻 𝑃 ) ∧ 𝐺 ∈ ( 𝑁 𝐽 𝑄 ) ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
42	15 16 41	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
43	38 40 42	oveq123d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ · ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) 𝐹 ) )
44		op2ndg	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌 ) → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
45	6 7 44	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
46		op2ndg	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌 ) → ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑄 )
47	8 9 46	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) = 𝑄 )
48	45 47	opeq12d	⊢ ( 𝜑 → ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ = ⟨ 𝑁 , 𝑄 ⟩ )
49		op2ndg	⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌 ) → ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑆 )
50	13 14 49	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑆 )
51	48 50	oveq12d	⊢ ( 𝜑 → ( ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ ∙ ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) = ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) )
52		op2ndg	⊢ ( ( 𝐾 ∈ ( 𝑃 𝐻 𝑅 ) ∧ 𝐿 ∈ ( 𝑄 𝐽 𝑆 ) ) → ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
53	17 18 52	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
54		op2ndg	⊢ ( ( 𝐹 ∈ ( 𝑀 𝐻 𝑃 ) ∧ 𝐺 ∈ ( 𝑁 𝐽 𝑄 ) ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
55	15 16 54	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
56	51 53 55	oveq123d	⊢ ( 𝜑 → ( ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ ∙ ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) 𝐺 ) )
57	43 56	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 1st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 1st ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ · ( 1st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ⟨ ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) , ( 2nd ‘ ⟨ 𝑃 , 𝑄 ⟩ ) ⟩ ∙ ( 2nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) ⟩ = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) 𝐺 ) ⟩ )
58	30 57	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ · 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ∙ 𝑆 ) 𝐺 ) ⟩ )