xpcco

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

	Ref	Expression
Hypotheses	xpccofval.t	$⊢ T = C \times_{c} D$
	xpccofval.b	$⊢ B = {Base}_{T}$
	xpccofval.k	$⊢ K = Hom (T)$
	xpccofval.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
	xpccofval.o2	$⊢ \underset{˙}{∙} = comp (D)$
	xpccofval.o	$⊢ O = comp (T)$
	xpcco.x	$⊢ φ \to X \in B$
	xpcco.y	$⊢ φ \to Y \in B$
	xpcco.z	$⊢ φ \to Z \in B$
	xpcco.f	$⊢ φ \to F \in (X K Y)$
	xpcco.g	$⊢ φ \to G \in (Y K Z)$
Assertion	xpcco	$⊢ φ \to G (⟨X, Y⟩ O Z) F = ⟨1^{st} (G) (⟨1^{st} (X), 1^{st} (Y)⟩ \underset{˙}{\cdot} 1^{st} (Z)) 1^{st} (F), 2^{nd} (G) (⟨2^{nd} (X), 2^{nd} (Y)⟩ \underset{˙}{∙} 2^{nd} (Z)) 2^{nd} (F)⟩$

Proof

Step	Hyp	Ref	Expression
1		xpccofval.t	$⊢ T = C \times_{c} D$
2		xpccofval.b	$⊢ B = {Base}_{T}$
3		xpccofval.k	$⊢ K = Hom (T)$
4		xpccofval.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
5		xpccofval.o2	$⊢ \underset{˙}{∙} = comp (D)$
6		xpccofval.o	$⊢ O = comp (T)$
7		xpcco.x	$⊢ φ \to X \in B$
8		xpcco.y	$⊢ φ \to Y \in B$
9		xpcco.z	$⊢ φ \to Z \in B$
10		xpcco.f	$⊢ φ \to F \in (X K Y)$
11		xpcco.g	$⊢ φ \to G \in (Y K Z)$
12	1 2 3 4 5 6	xpccofval	$⊢ O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩))$
13	7 8	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
14	9	adantr	$⊢ (φ \land x = ⟨X, Y⟩) \to Z \in B$
15		ovex	$⊢ 2^{nd} (x) K y \in V$
16		fvex	$⊢ K (x) \in V$
17	15 16	mpoex	$⊢ (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩) \in V$
18	17	a1i	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩) \in V$
19	11	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to G \in (Y K Z)$
20		simprl	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to x = ⟨X, Y⟩$
21	20	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to 2^{nd} (x) = 2^{nd} (⟨X, Y⟩)$
22		op2ndg	$⊢ (X \in B \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
23	7 8 22	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
24	23	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to 2^{nd} (⟨X, Y⟩) = Y$
25	21 24	eqtrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to 2^{nd} (x) = Y$
26		simprr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to y = Z$
27	25 26	oveq12d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to 2^{nd} (x) K y = Y K Z$
28	19 27	eleqtrrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to G \in (2^{nd} (x) K y)$
29	10	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to F \in (X K Y)$
30	20	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to K (x) = K (⟨X, Y⟩)$
31		df-ov	$⊢ X K Y = K (⟨X, Y⟩)$
32	30 31	syl6eqr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to K (x) = X K Y$
33	29 32	eleqtrrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to F \in K (x)$
34	33	adantr	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land g = G) \to F \in K (x)$
35		opex	$⊢ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩ \in V$
36	35	a1i	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩ \in V$
37	20	fveq2d	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to 1^{st} (x) = 1^{st} (⟨X, Y⟩)$
38		op1stg	$⊢ (X \in B \land Y \in B) \to 1^{st} (⟨X, Y⟩) = X$
39	7 8 38	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
40	39	adantr	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to 1^{st} (⟨X, Y⟩) = X$
41	37 40	eqtrd	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to 1^{st} (x) = X$
42	41	adantr	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 1^{st} (x) = X$
43	42	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 1^{st} (1^{st} (x)) = 1^{st} (X)$
44	25	adantr	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 2^{nd} (x) = Y$
45	44	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 1^{st} (2^{nd} (x)) = 1^{st} (Y)$
46	43 45	opeq12d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to ⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ = ⟨1^{st} (X), 1^{st} (Y)⟩$
47		simplrr	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to y = Z$
48	47	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 1^{st} (y) = 1^{st} (Z)$
49	46 48	oveq12d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to ⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y) = ⟨1^{st} (X), 1^{st} (Y)⟩ \underset{˙}{\cdot} 1^{st} (Z)$
50		simprl	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to g = G$
51	50	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 1^{st} (g) = 1^{st} (G)$
52		simprr	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to f = F$
53	52	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 1^{st} (f) = 1^{st} (F)$
54	49 51 53	oveq123d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f) = 1^{st} (G) (⟨1^{st} (X), 1^{st} (Y)⟩ \underset{˙}{\cdot} 1^{st} (Z)) 1^{st} (F)$
55	42	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 2^{nd} (1^{st} (x)) = 2^{nd} (X)$
56	44	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 2^{nd} (2^{nd} (x)) = 2^{nd} (Y)$
57	55 56	opeq12d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to ⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ = ⟨2^{nd} (X), 2^{nd} (Y)⟩$
58	47	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 2^{nd} (y) = 2^{nd} (Z)$
59	57 58	oveq12d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to ⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y) = ⟨2^{nd} (X), 2^{nd} (Y)⟩ \underset{˙}{∙} 2^{nd} (Z)$
60	50	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 2^{nd} (g) = 2^{nd} (G)$
61	52	fveq2d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 2^{nd} (f) = 2^{nd} (F)$
62	59 60 61	oveq123d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f) = 2^{nd} (G) (⟨2^{nd} (X), 2^{nd} (Y)⟩ \underset{˙}{∙} 2^{nd} (Z)) 2^{nd} (F)$
63	54 62	opeq12d	$⊢ ((φ \land (x = ⟨X, Y⟩ \land y = Z)) \land (g = G \land f = F)) \to ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩ = ⟨1^{st} (G) (⟨1^{st} (X), 1^{st} (Y)⟩ \underset{˙}{\cdot} 1^{st} (Z)) 1^{st} (F), 2^{nd} (G) (⟨2^{nd} (X), 2^{nd} (Y)⟩ \underset{˙}{∙} 2^{nd} (Z)) 2^{nd} (F)⟩$
64	28 34 36 63	ovmpodv2	$⊢ (φ \land (x = ⟨X, Y⟩ \land y = Z)) \to (⟨X, Y⟩ O Z = (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩) \to G (⟨X, Y⟩ O Z) F = ⟨1^{st} (G) (⟨1^{st} (X), 1^{st} (Y)⟩ \underset{˙}{\cdot} 1^{st} (Z)) 1^{st} (F), 2^{nd} (G) (⟨2^{nd} (X), 2^{nd} (Y)⟩ \underset{˙}{∙} 2^{nd} (Z)) 2^{nd} (F)⟩)$
65	13 14 18 64	ovmpodv	$⊢ φ \to (O = (x \in (B \times B), y \in B ⟼ (g \in (2^{nd} (x) K y), f \in K (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ \underset{˙}{\cdot} 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ \underset{˙}{∙} 2^{nd} (y)) 2^{nd} (f)⟩)) \to G (⟨X, Y⟩ O Z) F = ⟨1^{st} (G) (⟨1^{st} (X), 1^{st} (Y)⟩ \underset{˙}{\cdot} 1^{st} (Z)) 1^{st} (F), 2^{nd} (G) (⟨2^{nd} (X), 2^{nd} (Y)⟩ \underset{˙}{∙} 2^{nd} (Z)) 2^{nd} (F)⟩)$
66	12 65	mpi	$⊢ φ \to G (⟨X, Y⟩ O Z) F = ⟨1^{st} (G) (⟨1^{st} (X), 1^{st} (Y)⟩ \underset{˙}{\cdot} 1^{st} (Z)) 1^{st} (F), 2^{nd} (G) (⟨2^{nd} (X), 2^{nd} (Y)⟩ \underset{˙}{∙} 2^{nd} (Z)) 2^{nd} (F)⟩$

Metamath Proof Explorer

Theorem xpcco

Proof