fucoco2

Description: Composition in the source category is mapped to composition in the target. See also fucoco . (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fucoco2.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
	fucoco2.q	$⊢ Q = C FuncCat E$
	fucoco2.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fucoco2.1	$⊢ \underset{˙}{\cdot} = comp (T)$
	fucoco2.2	$⊢ \underset{˙}{∙} = comp (Q)$
	fucoco2.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
	fucoco2.x	$⊢ φ \to X \in W$
	fucoco2.y	$⊢ φ \to Y \in W$
	fucoco2.z	$⊢ φ \to Z \in W$
	fucoco2.j	$⊢ J = Hom (T)$
	fucoco2.a	$⊢ φ \to A \in (X J Y)$
	fucoco2.b	$⊢ φ \to B \in (Y J Z)$
Assertion	fucoco2	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (Y P Z) (B) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (A)$

Proof

Step	Hyp	Ref	Expression
1		fucoco2.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
2		fucoco2.q	$⊢ Q = C FuncCat E$
3		fucoco2.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
4		fucoco2.1	$⊢ \underset{˙}{\cdot} = comp (T)$
5		fucoco2.2	$⊢ \underset{˙}{∙} = comp (Q)$
6		fucoco2.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
7		fucoco2.x	$⊢ φ \to X \in W$
8		fucoco2.y	$⊢ φ \to Y \in W$
9		fucoco2.z	$⊢ φ \to Z \in W$
10		fucoco2.j	$⊢ J = Hom (T)$
11		fucoco2.a	$⊢ φ \to A \in (X J Y)$
12		fucoco2.b	$⊢ φ \to B \in (Y J Z)$
13	1	xpcfucbas	$⊢ (D Func E) \times (C Func D) = {Base}_{T}$
14	7 6	eleqtrd	$⊢ φ \to X \in ((D Func E) \times (C Func D))$
15	8 6	eleqtrd	$⊢ φ \to Y \in ((D Func E) \times (C Func D))$
16	1 13 10 14 15	xpcfuchom	$⊢ φ \to X J Y = (1^{st} (X) (D Nat E) 1^{st} (Y)) \times (2^{nd} (X) (C Nat D) 2^{nd} (Y))$
17	11 16	eleqtrd	$⊢ φ \to A \in ((1^{st} (X) (D Nat E) 1^{st} (Y)) \times (2^{nd} (X) (C Nat D) 2^{nd} (Y)))$
18		xp1st	$⊢ A \in ((1^{st} (X) (D Nat E) 1^{st} (Y)) \times (2^{nd} (X) (C Nat D) 2^{nd} (Y))) \to 1^{st} (A) \in (1^{st} (X) (D Nat E) 1^{st} (Y))$
19	17 18	syl	$⊢ φ \to 1^{st} (A) \in (1^{st} (X) (D Nat E) 1^{st} (Y))$
20		xp2nd	$⊢ A \in ((1^{st} (X) (D Nat E) 1^{st} (Y)) \times (2^{nd} (X) (C Nat D) 2^{nd} (Y))) \to 2^{nd} (A) \in (2^{nd} (X) (C Nat D) 2^{nd} (Y))$
21	17 20	syl	$⊢ φ \to 2^{nd} (A) \in (2^{nd} (X) (C Nat D) 2^{nd} (Y))$
22	9 6	eleqtrd	$⊢ φ \to Z \in ((D Func E) \times (C Func D))$
23	1 13 10 15 22	xpcfuchom	$⊢ φ \to Y J Z = (1^{st} (Y) (D Nat E) 1^{st} (Z)) \times (2^{nd} (Y) (C Nat D) 2^{nd} (Z))$
24	12 23	eleqtrd	$⊢ φ \to B \in ((1^{st} (Y) (D Nat E) 1^{st} (Z)) \times (2^{nd} (Y) (C Nat D) 2^{nd} (Z)))$
25		xp1st	$⊢ B \in ((1^{st} (Y) (D Nat E) 1^{st} (Z)) \times (2^{nd} (Y) (C Nat D) 2^{nd} (Z))) \to 1^{st} (B) \in (1^{st} (Y) (D Nat E) 1^{st} (Z))$
26	24 25	syl	$⊢ φ \to 1^{st} (B) \in (1^{st} (Y) (D Nat E) 1^{st} (Z))$
27		xp2nd	$⊢ B \in ((1^{st} (Y) (D Nat E) 1^{st} (Z)) \times (2^{nd} (Y) (C Nat D) 2^{nd} (Z))) \to 2^{nd} (B) \in (2^{nd} (Y) (C Nat D) 2^{nd} (Z))$
28	24 27	syl	$⊢ φ \to 2^{nd} (B) \in (2^{nd} (Y) (C Nat D) 2^{nd} (Z))$
29		1st2nd2	$⊢ X \in ((D Func E) \times (C Func D)) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
30	14 29	syl	$⊢ φ \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
31		1st2nd2	$⊢ Y \in ((D Func E) \times (C Func D)) \to Y = ⟨1^{st} (Y), 2^{nd} (Y)⟩$
32	15 31	syl	$⊢ φ \to Y = ⟨1^{st} (Y), 2^{nd} (Y)⟩$
33		1st2nd2	$⊢ Z \in ((D Func E) \times (C Func D)) \to Z = ⟨1^{st} (Z), 2^{nd} (Z)⟩$
34	22 33	syl	$⊢ φ \to Z = ⟨1^{st} (Z), 2^{nd} (Z)⟩$
35		1st2nd2	$⊢ A \in ((1^{st} (X) (D Nat E) 1^{st} (Y)) \times (2^{nd} (X) (C Nat D) 2^{nd} (Y))) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
36	17 35	syl	$⊢ φ \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
37		1st2nd2	$⊢ B \in ((1^{st} (Y) (D Nat E) 1^{st} (Z)) \times (2^{nd} (Y) (C Nat D) 2^{nd} (Z))) \to B = ⟨1^{st} (B), 2^{nd} (B)⟩$
38	24 37	syl	$⊢ φ \to B = ⟨1^{st} (B), 2^{nd} (B)⟩$
39	19 21 26 28 3 30 32 34 36 38 2 5 1 4	fucoco	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (Y P Z) (B) (⟨O (X), O (Y)⟩ \underset{˙}{∙} O (Z)) (X P Y) (A)$

Metamath Proof Explorer

Theorem fucoco2

Proof