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		eqid	$⊢ D Nat E = D Nat E$
14	13	natrcl	$⊢ R \in (F (D Nat E) K) \to (F \in (D Func E) \land K \in (D Func E))$
15	1 14	syl	$⊢ φ \to (F \in (D Func E) \land K \in (D Func E))$
16	15	simpld	$⊢ φ \to F \in (D Func E)$
17	16	func1st2nd	$⊢ φ \to 1^{st} (F) (D Func E) 2^{nd} (F)$
18	17	funcrcl3	$⊢ φ \to E \in Cat$
19		eqid	$⊢ {Base}_{D} = {Base}_{D}$
20	19 10 17	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{D} ⟶ {Base}_{E}$
21		eqid	$⊢ {Base}_{C} = {Base}_{C}$
22		eqid	$⊢ C Nat D = C Nat D$
23	22	natrcl	$⊢ S \in (G (C Nat D) L) \to (G \in (C Func D) \land L \in (C Func D))$
24	2 23	syl	$⊢ φ \to (G \in (C Func D) \land L \in (C Func D))$
25	24	simpld	$⊢ φ \to G \in (C Func D)$
26	25	func1st2nd	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
27	21 19 26	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
28	27 5	ffvelcdmd	$⊢ φ \to 1^{st} (G) (X) \in {Base}_{D}$
29	20 28	ffvelcdmd	$⊢ φ \to 1^{st} (F) (1^{st} (G) (X)) \in {Base}_{E}$
30	6	func1st2nd	$⊢ φ \to 1^{st} (P) (D Func E) 2^{nd} (P)$
31	19 10 30	funcf1	$⊢ φ \to 1^{st} (P) : {Base}_{D} ⟶ {Base}_{E}$
32	7	func1st2nd	$⊢ φ \to 1^{st} (Q) (C Func D) 2^{nd} (Q)$
33	21 19 32	funcf1	$⊢ φ \to 1^{st} (Q) : {Base}_{C} ⟶ {Base}_{D}$
34	33 5	ffvelcdmd	$⊢ φ \to 1^{st} (Q) (X) \in {Base}_{D}$
35	31 34	ffvelcdmd	$⊢ φ \to 1^{st} (P) (1^{st} (Q) (X)) \in {Base}_{E}$
36	15	simprd	$⊢ φ \to K \in (D Func E)$
37	36	func1st2nd	$⊢ φ \to 1^{st} (K) (D Func E) 2^{nd} (K)$
38	19 10 37	funcf1	$⊢ φ \to 1^{st} (K) : {Base}_{D} ⟶ {Base}_{E}$
39	22	natrcl	$⊢ V \in (L (C Nat D) N) \to (L \in (C Func D) \land N \in (C Func D))$
40	4 39	syl	$⊢ φ \to (L \in (C Func D) \land N \in (C Func D))$
41	40	simprd	$⊢ φ \to N \in (C Func D)$
42	41	func1st2nd	$⊢ φ \to 1^{st} (N) (C Func D) 2^{nd} (N)$
43	21 19 42	funcf1	$⊢ φ \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
44	43 5	ffvelcdmd	$⊢ φ \to 1^{st} (N) (X) \in {Base}_{D}$
45	38 44	ffvelcdmd	$⊢ φ \to 1^{st} (K) (1^{st} (N) (X)) \in {Base}_{E}$
46	24	simprd	$⊢ φ \to L \in (C Func D)$
47	46	func1st2nd	$⊢ φ \to 1^{st} (L) (C Func D) 2^{nd} (L)$
48	21 19 47	funcf1	$⊢ φ \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
49	48 5	ffvelcdmd	$⊢ φ \to 1^{st} (L) (X) \in {Base}_{D}$
50	20 49	ffvelcdmd	$⊢ φ \to 1^{st} (F) (1^{st} (L) (X)) \in {Base}_{E}$
51		eqid	$⊢ Hom (D) = Hom (D)$
52	19 51 11 17 28 49	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))$
53	22 2	nat1st2nd	$⊢ φ \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ (C Nat D) ⟨1^{st} (L), 2^{nd} (L)⟩)$
54	22 53 21 51 5	natcl	$⊢ φ \to S (X) \in (1^{st} (G) (X) Hom (D) 1^{st} (L) (X))$
55	52 54	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)))$
56	10 11 12 18 29 50 35 55 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)))$
57	13	natrcl	$⊢ U \in (K (D Nat E) M) \to (K \in (D Func E) \land M \in (D Func E))$
58	3 57	syl	$⊢ φ \to (K \in (D Func E) \land M \in (D Func E))$
59	58	simprd	$⊢ φ \to M \in (D Func E)$
60	59	func1st2nd	$⊢ φ \to 1^{st} (M) (D Func E) 2^{nd} (M)$
61	19 10 60	funcf1	$⊢ φ \to 1^{st} (M) : {Base}_{D} ⟶ {Base}_{E}$
62	61 44	ffvelcdmd	$⊢ φ \to 1^{st} (M) (1^{st} (N) (X)) \in {Base}_{E}$
63	13 3	nat1st2nd	$⊢ φ \to U \in (⟨1^{st} (K), 2^{nd} (K)⟩ (D Nat E) ⟨1^{st} (M), 2^{nd} (M)⟩)$
64	13 63 19 11 44	natcl	$⊢ φ \to U (1^{st} (N) (X)) \in (1^{st} (K) (1^{st} (N) (X)) Hom (E) 1^{st} (M) (1^{st} (N) (X)))$
65	10 11 12 18 29 35 45 56 8 62 64	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))))$
66	10 11 12 18 29 50 35 55 9 45 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)))$
67	66	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))))$
68	65 67	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