xpcfucco3

Description: Value of composition in the binary product of categories of functors; expressed explicitly. (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypotheses	xpcfuchom2.t	$⊢ T = (B FuncCat C) \times_{c} (D FuncCat E)$
	xpcfucco2.o	$⊢ O = comp (T)$
	xpcfucco2.f	$⊢ φ \to F \in (M (B Nat C) P)$
	xpcfucco2.g	$⊢ φ \to G \in (N (D Nat E) Q)$
	xpcfucco2.k	$⊢ φ \to K \in (P (B Nat C) R)$
	xpcfucco2.l	$⊢ φ \to L \in (Q (D Nat E) S)$
	xpcfucco3.x	$⊢ X = {Base}_{B}$
	xpcfucco3.y	$⊢ Y = {Base}_{D}$
	xpcfucco3.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
	xpcfucco3.o2	$⊢ \underset{˙}{∙} = comp (E)$
Assertion	xpcfucco3	$⊢ φ \to ⟨K, L⟩ (⟨⟨M, N⟩, ⟨P, Q⟩⟩ O ⟨R, S⟩) ⟨F, G⟩ = ⟨(x \in X ⟼ K (x) (⟨1^{st} (M) (x), 1^{st} (P) (x)⟩ \underset{˙}{\cdot} 1^{st} (R) (x)) F (x)), (y \in Y ⟼ L (y) (⟨1^{st} (N) (y), 1^{st} (Q) (y)⟩ \underset{˙}{∙} 1^{st} (S) (y)) G (y))⟩$

Proof

Step	Hyp	Ref	Expression
1		xpcfuchom2.t	$⊢ T = (B FuncCat C) \times_{c} (D FuncCat E)$
2		xpcfucco2.o	$⊢ O = comp (T)$
3		xpcfucco2.f	$⊢ φ \to F \in (M (B Nat C) P)$
4		xpcfucco2.g	$⊢ φ \to G \in (N (D Nat E) Q)$
5		xpcfucco2.k	$⊢ φ \to K \in (P (B Nat C) R)$
6		xpcfucco2.l	$⊢ φ \to L \in (Q (D Nat E) S)$
7		xpcfucco3.x	$⊢ X = {Base}_{B}$
8		xpcfucco3.y	$⊢ Y = {Base}_{D}$
9		xpcfucco3.o1	$⊢ \underset{˙}{\cdot} = comp (C)$
10		xpcfucco3.o2	$⊢ \underset{˙}{∙} = comp (E)$
11	1 2 3 4 5 6	xpcfucco2	$⊢ φ \to ⟨K, L⟩ (⟨⟨M, N⟩, ⟨P, Q⟩⟩ O ⟨R, S⟩) ⟨F, G⟩ = ⟨K (⟨M, P⟩ comp (B FuncCat C) R) F, L (⟨N, Q⟩ comp (D FuncCat E) S) G⟩$
12		eqid	$⊢ B FuncCat C = B FuncCat C$
13		eqid	$⊢ B Nat C = B Nat C$
14		eqid	$⊢ comp (B FuncCat C) = comp (B FuncCat C)$
15	12 13 7 9 14 3 5	fucco	$⊢ φ \to K (⟨M, P⟩ comp (B FuncCat C) R) F = (x \in X ⟼ K (x) (⟨1^{st} (M) (x), 1^{st} (P) (x)⟩ \underset{˙}{\cdot} 1^{st} (R) (x)) F (x))$
16		eqid	$⊢ D FuncCat E = D FuncCat E$
17		eqid	$⊢ D Nat E = D Nat E$
18		eqid	$⊢ comp (D FuncCat E) = comp (D FuncCat E)$
19	16 17 8 10 18 4 6	fucco	$⊢ φ \to L (⟨N, Q⟩ comp (D FuncCat E) S) G = (y \in Y ⟼ L (y) (⟨1^{st} (N) (y), 1^{st} (Q) (y)⟩ \underset{˙}{∙} 1^{st} (S) (y)) G (y))$
20	15 19	opeq12d	$⊢ φ \to ⟨K (⟨M, P⟩ comp (B FuncCat C) R) F, L (⟨N, Q⟩ comp (D FuncCat E) S) G⟩ = ⟨(x \in X ⟼ K (x) (⟨1^{st} (M) (x), 1^{st} (P) (x)⟩ \underset{˙}{\cdot} 1^{st} (R) (x)) F (x)), (y \in Y ⟼ L (y) (⟨1^{st} (N) (y), 1^{st} (Q) (y)⟩ \underset{˙}{∙} 1^{st} (S) (y)) G (y))⟩$
21	11 20	eqtrd	$⊢ φ \to ⟨K, L⟩ (⟨⟨M, N⟩, ⟨P, Q⟩⟩ O ⟨R, S⟩) ⟨F, G⟩ = ⟨(x \in X ⟼ K (x) (⟨1^{st} (M) (x), 1^{st} (P) (x)⟩ \underset{˙}{\cdot} 1^{st} (R) (x)) F (x)), (y \in Y ⟼ L (y) (⟨1^{st} (N) (y), 1^{st} (Q) (y)⟩ \underset{˙}{∙} 1^{st} (S) (y)) G (y))⟩$

Metamath Proof Explorer

Theorem xpcfucco3

Proof