fucocolem1

Description: Lemma for fucoco . Associativity for morphisms in category E . To simply put, ( ( a .x. b ) .x. ( c .x. d ) ) = ( a .x. ( ( b .x. c ) .x. d ) ) for morphism compositions. (Contributed by Zhi Wang, 2-Oct-2025)

	Ref	Expression
Hypotheses	fucoco.r	$⊢ φ \to R \in (F (D Nat E) K)$
	fucoco.s	$⊢ φ \to S \in (G (C Nat D) L)$
	fucoco.u	$⊢ φ \to U \in (K (D Nat E) M)$
	fucoco.v	$⊢ φ \to V \in (L (C Nat D) N)$
	fucocolem1.x	$⊢ φ \to X \in {Base}_{C}$
	fucocolem1.p	$⊢ φ \to P \in (D Func E)$
	fucocolem1.q	$⊢ φ \to Q \in (C Func D)$
	fucocolem1.a	$⊢ φ \to A \in (1^{st} (P) (1^{st} (Q) (X)) Hom (E) 1^{st} (K) (1^{st} (N) (X)))$
	fucocolem1.b	$⊢ φ \to B \in (1^{st} (F) (1^{st} (L) (X)) Hom (E) 1^{st} (P) (1^{st} (Q) (X)))$
Assertion	fucocolem1	$⊢ φ \to (U (1^{st} (N) (X)) (⟨1^{st} (P) (1^{st} (Q) (X)), 1^{st} (K) (1^{st} (N) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) A) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) (B (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (P) (1^{st} (Q) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X))) = U (1^{st} (N) (X)) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (K) (1^{st} (N) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) ((A (⟨1^{st} (F) (1^{st} (L) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) B) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X)))$

Proof

Step	Hyp	Ref	Expression
1		fucoco.r	$⊢ φ \to R \in (F (D Nat E) K)$
2		fucoco.s	$⊢ φ \to S \in (G (C Nat D) L)$
3		fucoco.u	$⊢ φ \to U \in (K (D Nat E) M)$
4		fucoco.v	$⊢ φ \to V \in (L (C Nat D) N)$
5		fucocolem1.x	$⊢ φ \to X \in {Base}_{C}$
6		fucocolem1.p	$⊢ φ \to P \in (D Func E)$
7		fucocolem1.q	$⊢ φ \to Q \in (C Func D)$
8		fucocolem1.a	$⊢ φ \to A \in (1^{st} (P) (1^{st} (Q) (X)) Hom (E) 1^{st} (K) (1^{st} (N) (X)))$
9		fucocolem1.b	$⊢ φ \to B \in (1^{st} (F) (1^{st} (L) (X)) Hom (E) 1^{st} (P) (1^{st} (Q) (X)))$
10		eqid	$⊢ {Base}_{E} = {Base}_{E}$
11		eqid	$⊢ Hom (E) = Hom (E)$
12		eqid	$⊢ comp (E) = comp (E)$
13		relfunc	$⊢ Rel (D Func E)$
14		eqid	$⊢ D Nat E = D Nat E$
15	14	natrcl	$⊢ R \in (F (D Nat E) K) \to (F \in (D Func E) \land K \in (D Func E))$
16	1 15	syl	$⊢ φ \to (F \in (D Func E) \land K \in (D Func E))$
17	16	simpld	$⊢ φ \to F \in (D Func E)$
18		1st2ndbr	$⊢ (Rel (D Func E) \land F \in (D Func E)) \to 1^{st} (F) (D Func E) 2^{nd} (F)$
19	13 17 18	sylancr	$⊢ φ \to 1^{st} (F) (D Func E) 2^{nd} (F)$
20	19	funcrcl3	$⊢ φ \to E \in Cat$
21		eqid	$⊢ {Base}_{D} = {Base}_{D}$
22	21 10 19	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{D} ⟶ {Base}_{E}$
23		eqid	$⊢ {Base}_{C} = {Base}_{C}$
24		relfunc	$⊢ Rel (C Func D)$
25		eqid	$⊢ C Nat D = C Nat D$
26	25	natrcl	$⊢ S \in (G (C Nat D) L) \to (G \in (C Func D) \land L \in (C Func D))$
27	2 26	syl	$⊢ φ \to (G \in (C Func D) \land L \in (C Func D))$
28	27	simpld	$⊢ φ \to G \in (C Func D)$
29		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
30	24 28 29	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
31	23 21 30	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
32	31 5	ffvelcdmd	$⊢ φ \to 1^{st} (G) (X) \in {Base}_{D}$
33	22 32	ffvelcdmd	$⊢ φ \to 1^{st} (F) (1^{st} (G) (X)) \in {Base}_{E}$
34		1st2ndbr	$⊢ (Rel (D Func E) \land P \in (D Func E)) \to 1^{st} (P) (D Func E) 2^{nd} (P)$
35	13 6 34	sylancr	$⊢ φ \to 1^{st} (P) (D Func E) 2^{nd} (P)$
36	21 10 35	funcf1	$⊢ φ \to 1^{st} (P) : {Base}_{D} ⟶ {Base}_{E}$
37		1st2ndbr	$⊢ (Rel (C Func D) \land Q \in (C Func D)) \to 1^{st} (Q) (C Func D) 2^{nd} (Q)$
38	24 7 37	sylancr	$⊢ φ \to 1^{st} (Q) (C Func D) 2^{nd} (Q)$
39	23 21 38	funcf1	$⊢ φ \to 1^{st} (Q) : {Base}_{C} ⟶ {Base}_{D}$
40	39 5	ffvelcdmd	$⊢ φ \to 1^{st} (Q) (X) \in {Base}_{D}$
41	36 40	ffvelcdmd	$⊢ φ \to 1^{st} (P) (1^{st} (Q) (X)) \in {Base}_{E}$
42	16	simprd	$⊢ φ \to K \in (D Func E)$
43		1st2ndbr	$⊢ (Rel (D Func E) \land K \in (D Func E)) \to 1^{st} (K) (D Func E) 2^{nd} (K)$
44	13 42 43	sylancr	$⊢ φ \to 1^{st} (K) (D Func E) 2^{nd} (K)$
45	21 10 44	funcf1	$⊢ φ \to 1^{st} (K) : {Base}_{D} ⟶ {Base}_{E}$
46	25	natrcl	$⊢ V \in (L (C Nat D) N) \to (L \in (C Func D) \land N \in (C Func D))$
47	4 46	syl	$⊢ φ \to (L \in (C Func D) \land N \in (C Func D))$
48	47	simprd	$⊢ φ \to N \in (C Func D)$
49		1st2ndbr	$⊢ (Rel (C Func D) \land N \in (C Func D)) \to 1^{st} (N) (C Func D) 2^{nd} (N)$
50	24 48 49	sylancr	$⊢ φ \to 1^{st} (N) (C Func D) 2^{nd} (N)$
51	23 21 50	funcf1	$⊢ φ \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
52	51 5	ffvelcdmd	$⊢ φ \to 1^{st} (N) (X) \in {Base}_{D}$
53	45 52	ffvelcdmd	$⊢ φ \to 1^{st} (K) (1^{st} (N) (X)) \in {Base}_{E}$
54	27	simprd	$⊢ φ \to L \in (C Func D)$
55		1st2ndbr	$⊢ (Rel (C Func D) \land L \in (C Func D)) \to 1^{st} (L) (C Func D) 2^{nd} (L)$
56	24 54 55	sylancr	$⊢ φ \to 1^{st} (L) (C Func D) 2^{nd} (L)$
57	23 21 56	funcf1	$⊢ φ \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
58	57 5	ffvelcdmd	$⊢ φ \to 1^{st} (L) (X) \in {Base}_{D}$
59	22 58	ffvelcdmd	$⊢ φ \to 1^{st} (F) (1^{st} (L) (X)) \in {Base}_{E}$
60		eqid	$⊢ Hom (D) = Hom (D)$
61	21 60 11 19 32 58	funcf2	$⊢ φ \to (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) : 1^{st} (G) (X) Hom (D) 1^{st} (L) (X) ⟶ 1^{st} (F) (1^{st} (G) (X)) Hom (E) 1^{st} (F) (1^{st} (L) (X))$
62	25 2	nat1st2nd	$⊢ φ \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ (C Nat D) ⟨1^{st} (L), 2^{nd} (L)⟩)$
63	25 62 23 60 5	natcl	$⊢ φ \to S (X) \in (1^{st} (G) (X) Hom (D) 1^{st} (L) (X))$
64	61 63	ffvelcdmd	$⊢ φ \to (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X)) \in (1^{st} (F) (1^{st} (G) (X)) Hom (E) 1^{st} (F) (1^{st} (L) (X)))$
65	10 11 12 20 33 59 41 64 9	catcocl	$⊢ φ \to B (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (P) (1^{st} (Q) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X)) \in (1^{st} (F) (1^{st} (G) (X)) Hom (E) 1^{st} (P) (1^{st} (Q) (X)))$
66	14	natrcl	$⊢ U \in (K (D Nat E) M) \to (K \in (D Func E) \land M \in (D Func E))$
67	3 66	syl	$⊢ φ \to (K \in (D Func E) \land M \in (D Func E))$
68	67	simprd	$⊢ φ \to M \in (D Func E)$
69		1st2ndbr	$⊢ (Rel (D Func E) \land M \in (D Func E)) \to 1^{st} (M) (D Func E) 2^{nd} (M)$
70	13 68 69	sylancr	$⊢ φ \to 1^{st} (M) (D Func E) 2^{nd} (M)$
71	21 10 70	funcf1	$⊢ φ \to 1^{st} (M) : {Base}_{D} ⟶ {Base}_{E}$
72	71 52	ffvelcdmd	$⊢ φ \to 1^{st} (M) (1^{st} (N) (X)) \in {Base}_{E}$
73	14 3	nat1st2nd	$⊢ φ \to U \in (⟨1^{st} (K), 2^{nd} (K)⟩ (D Nat E) ⟨1^{st} (M), 2^{nd} (M)⟩)$
74	14 73 21 11 52	natcl	$⊢ φ \to U (1^{st} (N) (X)) \in (1^{st} (K) (1^{st} (N) (X)) Hom (E) 1^{st} (M) (1^{st} (N) (X)))$
75	10 11 12 20 33 41 53 65 8 72 74	catass	$⊢ φ \to (U (1^{st} (N) (X)) (⟨1^{st} (P) (1^{st} (Q) (X)), 1^{st} (K) (1^{st} (N) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) A) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) (B (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (P) (1^{st} (Q) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X))) = U (1^{st} (N) (X)) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (K) (1^{st} (N) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) (A (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) (B (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (P) (1^{st} (Q) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X))))$
76	10 11 12 20 33 59 41 64 9 53 8	catass	$⊢ φ \to (A (⟨1^{st} (F) (1^{st} (L) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) B) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X)) = A (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) (B (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (P) (1^{st} (Q) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X)))$
77	76	oveq2d	$⊢ φ \to U (1^{st} (N) (X)) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (K) (1^{st} (N) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) ((A (⟨1^{st} (F) (1^{st} (L) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) B) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X))) = U (1^{st} (N) (X)) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (K) (1^{st} (N) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) (A (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) (B (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (P) (1^{st} (Q) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X))))$
78	75 77	eqtr4d	$⊢ φ \to (U (1^{st} (N) (X)) (⟨1^{st} (P) (1^{st} (Q) (X)), 1^{st} (K) (1^{st} (N) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) A) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) (B (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (P) (1^{st} (Q) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X))) = U (1^{st} (N) (X)) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (K) (1^{st} (N) (X))⟩ comp (E) 1^{st} (M) (1^{st} (N) (X))) ((A (⟨1^{st} (F) (1^{st} (L) (X)), 1^{st} (P) (1^{st} (Q) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) B) (⟨1^{st} (F) (1^{st} (G) (X)), 1^{st} (F) (1^{st} (L) (X))⟩ comp (E) 1^{st} (K) (1^{st} (N) (X))) (1^{st} (G) (X) 2^{nd} (F) 1^{st} (L) (X)) (S (X)))$

Metamath Proof Explorer

Theorem fucocolem1

Proof