fucocolem3

Description: Lemma for fucoco . The composed natural transformations are mapped to composition of 4 natural transformations. (Contributed by Zhi Wang, 3-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)$
	fucoco.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fucoco.x	$⊢ φ \to X = ⟨F, G⟩$
	fucoco.y	$⊢ φ \to Y = ⟨K, L⟩$
	fucoco.z	$⊢ φ \to Z = ⟨M, N⟩$
	fucoco.a	$⊢ φ \to A = ⟨R, S⟩$
	fucoco.b	$⊢ φ \to B = ⟨U, V⟩$
	fucocolem2.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
	fucocolem2.ot	$⊢ \underset{˙}{\cdot} = comp (T)$
	fucocolem2.od	$⊢ \underset{˙}{*} = comp (D)$
Assertion	fucocolem3	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (x \in {Base}_{C} ⟼ 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))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨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		fucoco.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 \|-
6		fucoco.x	$⊢ φ \to X = ⟨F, G⟩$
7		fucoco.y	$⊢ φ \to Y = ⟨K, L⟩$
8		fucoco.z	$⊢ φ \to Z = ⟨M, N⟩$
9		fucoco.a	$⊢ φ \to A = ⟨R, S⟩$
10		fucoco.b	$⊢ φ \to B = ⟨U, V⟩$
11		fucocolem2.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
12		fucocolem2.ot	$⊢ \underset{˙}{\cdot} = comp (T)$
13		fucocolem2.od	$⊢ \underset{˙}{*} = comp (D)$
14	1 2 3 4 5 6 7 8 9 10 11 12 13	fucocolem2	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (x \in {Base}_{C} ⟼ (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x)))$
15		eqid	$⊢ {Base}_{D} = {Base}_{D}$
16		eqid	$⊢ Hom (D) = Hom (D)$
17		eqid	$⊢ comp (E) = comp (E)$
18		eqid	$⊢ D Nat E = D Nat E$
19	18	natrcl	$⊢ R \in (F (D Nat E) K) \to (F \in (D Func E) \land K \in (D Func E))$
20	1 19	syl	$⊢ φ \to (F \in (D Func E) \land K \in (D Func E))$
21	20	simpld	$⊢ φ \to F \in (D Func E)$
22	21	func1st2nd	$⊢ φ \to 1^{st} (F) (D Func E) 2^{nd} (F)$
23	22	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (D Func E) 2^{nd} (F)$
24		eqid	$⊢ {Base}_{C} = {Base}_{C}$
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	28	func1st2nd	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
30	24 15 29	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
31	30	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) \in {Base}_{D}$
32	27	simprd	$⊢ φ \to L \in (C Func D)$
33	32	func1st2nd	$⊢ φ \to 1^{st} (L) (C Func D) 2^{nd} (L)$
34	24 15 33	funcf1	$⊢ φ \to 1^{st} (L) : {Base}_{C} ⟶ {Base}_{D}$
35	34	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (L) (x) \in {Base}_{D}$
36	25	natrcl	$⊢ V \in (L (C Nat D) N) \to (L \in (C Func D) \land N \in (C Func D))$
37	4 36	syl	$⊢ φ \to (L \in (C Func D) \land N \in (C Func D))$
38	37	simprd	$⊢ φ \to N \in (C Func D)$
39	38	func1st2nd	$⊢ φ \to 1^{st} (N) (C Func D) 2^{nd} (N)$
40	24 15 39	funcf1	$⊢ φ \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
41	40	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (N) (x) \in {Base}_{D}$
42	25 2	nat1st2nd	$⊢ φ \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ (C Nat D) ⟨1^{st} (L), 2^{nd} (L)⟩)$
43	42	adantr	$⊢ (φ \land x \in {Base}_{C}) \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ (C Nat D) ⟨1^{st} (L), 2^{nd} (L)⟩)$
44		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
45	25 43 24 16 44	natcl	$⊢ (φ \land x \in {Base}_{C}) \to S (x) \in (1^{st} (G) (x) Hom (D) 1^{st} (L) (x))$
46	25 4	nat1st2nd	$⊢ φ \to V \in (⟨1^{st} (L), 2^{nd} (L)⟩ (C Nat D) ⟨1^{st} (N), 2^{nd} (N)⟩)$
47	46	adantr	$⊢ (φ \land x \in {Base}_{C}) \to V \in (⟨1^{st} (L), 2^{nd} (L)⟩ (C Nat D) ⟨1^{st} (N), 2^{nd} (N)⟩)$
48	25 47 24 16 44	natcl	$⊢ (φ \land x \in {Base}_{C}) \to V (x) \in (1^{st} (L) (x) Hom (D) 1^{st} (N) (x))$
49	15 16 13 17 23 31 35 41 45 48	funcco	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x)) = (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (F) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x))$
50	49	oveq2d	$⊢ (φ \land x \in {Base}_{C}) \to (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x)) = (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (F) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (L) (x)) (S (x)))$
51	1	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R \in (F (D Nat E) K)$
52	2	adantr	$⊢ (φ \land x \in {Base}_{C}) \to S \in (G (C Nat D) L)$
53	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to U \in (K (D Nat E) M)$
54	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to V \in (L (C Nat D) N)$
55	21	adantr	$⊢ (φ \land x \in {Base}_{C}) \to F \in (D Func E)$
56	38	adantr	$⊢ (φ \land x \in {Base}_{C}) \to N \in (C Func D)$
57	18 1	nat1st2nd	$⊢ φ \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ (D Nat E) ⟨1^{st} (K), 2^{nd} (K)⟩)$
58	57	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ (D Nat E) ⟨1^{st} (K), 2^{nd} (K)⟩)$
59		eqid	$⊢ Hom (E) = Hom (E)$
60	18 58 15 59 41	natcl	$⊢ (φ \land x \in {Base}_{C}) \to R (1^{st} (N) (x)) \in (1^{st} (F) (1^{st} (N) (x)) Hom (E) 1^{st} (K) (1^{st} (N) (x)))$
61	15 16 59 23 35 41	funcf2	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) : 1^{st} (L) (x) Hom (D) 1^{st} (N) (x) ⟶ 1^{st} (F) (1^{st} (L) (x)) Hom (E) 1^{st} (F) (1^{st} (N) (x))$
62	61 48	ffvelcdmd	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x)) \in (1^{st} (F) (1^{st} (L) (x)) Hom (E) 1^{st} (F) (1^{st} (N) (x)))$
63	51 52 53 54 44 55 56 60 62	fucocolem1	$⊢ (φ \land x \in {Base}_{C}) \to (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) ((1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x)) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (L) (x))⟩ comp (E) 1^{st} (F) (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))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨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)))$
64	50 63	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (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))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨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)))$
65	64	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ (U (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) R (1^{st} (N) (x))) (⟨1^{st} (F) (1^{st} (G) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))) (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{*} 1^{st} (N) (x)) S (x))) = (x \in {Base}_{C} ⟼ 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))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨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))))$
66	14 65	eqtrd	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (x \in {Base}_{C} ⟼ 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))) ((R (1^{st} (N) (x)) (⟨1^{st} (F) (1^{st} (L) (x)), 1^{st} (F) (1^{st} (N) (x))⟩ comp (E) 1^{st} (K) (1^{st} (N) (x))) (1^{st} (L) (x) 2^{nd} (F) 1^{st} (N) (x)) (V (x))) (⟨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 fucocolem3

Proof