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 = {Base}_{C}$
	xpcco2.y	$⊢ Y = {Base}_{D}$
	xpcco2.h	$⊢ H = Hom (C)$
	xpcco2.j	$⊢ J = Hom (D)$
	xpcco2.m	$⊢ φ \to M \in X$
	xpcco2.n	$⊢ φ \to N \in Y$
	xpcco2.p	$⊢ φ \to P \in X$
	xpcco2.q	$⊢ φ \to Q \in Y$
	xpcco2.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
	xpcco2.o2	$⊢ \underset{˙}{∙} = comp (D)$
	xpcco2.o	$⊢ O = comp (T)$
	xpcco2.r	$⊢ φ \to R \in X$
	xpcco2.s	$⊢ φ \to S \in Y$
	xpcco2.f	$⊢ φ \to F \in (M H P)$
	xpcco2.g	$⊢ φ \to G \in (N J Q)$
	xpcco2.k	$⊢ φ \to K \in (P H R)$
	xpcco2.l	$⊢ φ \to L \in (Q J S)$
Assertion	xpcco2	$⊢ φ \to ⟨K, L⟩ (⟨⟨M, N⟩, ⟨P, Q⟩⟩ O ⟨R, S⟩) ⟨F, G⟩ = ⟨K (⟨M, P⟩ \underset{˙}{\cdot} R) F, L (⟨N, Q⟩ \underset{˙}{∙} S) G⟩$

Proof

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

Metamath Proof Explorer

Theorem xpcco2

Proof