fucocolem2

Description: Lemma for fucoco . The composed natural transformations are mapped to composition of 4 natural transformations. (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)$
	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	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)))$

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	6 7	opeq12d	$⊢ φ \to ⟨X, Y⟩ = ⟨⟨F, G⟩, ⟨K, L⟩⟩$
15	14 8	oveq12d	$⊢ φ \to ⟨X, Y⟩ \underset{˙}{\cdot} Z = ⟨⟨F, G⟩, ⟨K, L⟩⟩ \underset{˙}{\cdot} ⟨M, N⟩$
16	15 10 9	oveq123d	$⊢ φ \to B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A = ⟨U, V⟩ (⟨⟨F, G⟩, ⟨K, L⟩⟩ \underset{˙}{\cdot} ⟨M, N⟩) ⟨R, S⟩$
17		eqid	$⊢ {Base}_{D} = {Base}_{D}$
18		eqid	$⊢ {Base}_{C} = {Base}_{C}$
19		eqid	$⊢ comp (E) = comp (E)$
20	11 12 1 2 3 4 17 18 19 13	xpcfucco3	$⊢ φ \to ⟨U, V⟩ (⟨⟨F, G⟩, ⟨K, L⟩⟩ \underset{˙}{\cdot} ⟨M, N⟩) ⟨R, S⟩ = ⟨(p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)), (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{*} 1^{st} (N) (p)) S (p))⟩$
21	16 20	eqtrd	$⊢ φ \to B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A = ⟨(p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)), (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{*} 1^{st} (N) (p)) S (p))⟩$
22	21	fveq2d	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (X P Z) (⟨(p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)), (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{*} 1^{st} (N) (p)) S (p))⟩)$
23		df-ov	$⊢ (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) (X P Z) (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) = (X P Z) (⟨(p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)), (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p))⟩)$
24	22 23	eqtr4di	$⊢ φ \to (X P Z) (B (⟨X, Y⟩ \underset{˙}{\cdot} Z) A) = (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) (X P Z) (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{*} 1^{st} (N) (p)) S (p))$
25	11 12 1 2 3 4	xpcfuccocl	$⊢ φ \to ⟨U, V⟩ (⟨⟨F, G⟩, ⟨K, L⟩⟩ \underset{˙}{\cdot} ⟨M, N⟩) ⟨R, S⟩ \in ((F (D Nat E) M) \times (G (C Nat D) N))$
26	20 25	eqeltrrd	$⊢ φ \to ⟨(p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)), (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{*} 1^{st} (N) (p)) S (p))⟩ \in ((F (D Nat E) M) \times (G (C Nat D) N))$
27		opelxp2	$⊢ ⟨(p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)), (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p))⟩ \in ((F (D Nat E) M) \times (G (C Nat D) N)) \to (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) \in (G (C Nat D) N)$
28	26 27	syl	$⊢ φ \to (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{*} 1^{st} (N) (p)) S (p)) \in (G (C Nat D) N)$
29		opelxp1	$⊢ ⟨(p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)), (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{*} 1^{st} (N) (p)) S (p))⟩ \in ((F (D Nat E) M) \times (G (C Nat D) N)) \to (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) \in (F (D Nat E) M)$
30	26 29	syl	$⊢ φ \to (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) \in (F (D Nat E) M)$
31	5 6 8 28 30	fuco22a	$⊢ φ \to (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) (X P Z) (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) = (x \in {Base}_{C} ⟼ (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) (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)) ((p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) (x)))$
32		relfunc	$⊢ Rel (C Func D)$
33		eqid	$⊢ C Nat D = C Nat D$
34	33	natrcl	$⊢ V \in (L (C Nat D) N) \to (L \in (C Func D) \land N \in (C Func D))$
35	4 34	syl	$⊢ φ \to (L \in (C Func D) \land N \in (C Func D))$
36	35	simprd	$⊢ φ \to N \in (C Func D)$
37		1st2ndbr	$⊢ (Rel (C Func D) \land N \in (C Func D)) \to 1^{st} (N) (C Func D) 2^{nd} (N)$
38	32 36 37	sylancr	$⊢ φ \to 1^{st} (N) (C Func D) 2^{nd} (N)$
39	18 17 38	funcf1	$⊢ φ \to 1^{st} (N) : {Base}_{C} ⟶ {Base}_{D}$
40	39	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (N) (x) \in {Base}_{D}$
41		fveq2	$⊢ p = 1^{st} (N) (x) \to 1^{st} (F) (p) = 1^{st} (F) (1^{st} (N) (x))$
42		fveq2	$⊢ p = 1^{st} (N) (x) \to 1^{st} (K) (p) = 1^{st} (K) (1^{st} (N) (x))$
43	41 42	opeq12d	$⊢ p = 1^{st} (N) (x) \to ⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ = ⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩$
44		fveq2	$⊢ p = 1^{st} (N) (x) \to 1^{st} (M) (p) = 1^{st} (M) (1^{st} (N) (x))$
45	43 44	oveq12d	$⊢ p = 1^{st} (N) (x) \to ⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p) = ⟨1^{st} (F) (1^{st} (N) (x)), 1^{st} (K) (1^{st} (N) (x))⟩ comp (E) 1^{st} (M) (1^{st} (N) (x))$
46		fveq2	$⊢ p = 1^{st} (N) (x) \to U (p) = U (1^{st} (N) (x))$
47		fveq2	$⊢ p = 1^{st} (N) (x) \to R (p) = R (1^{st} (N) (x))$
48	45 46 47	oveq123d	$⊢ p = 1^{st} (N) (x) \to U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p) = 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))$
49		eqid	$⊢ (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) = (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p))$
50		ovex	$⊢ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p) \in V$
51	48 49 50	fvmpt3i	$⊢ 1^{st} (N) (x) \in {Base}_{D} \to (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) (1^{st} (N) (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))$
52	40 51	syl	$⊢ (φ \land x \in {Base}_{C}) \to (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) (1^{st} (N) (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))$
53		fveq2	$⊢ p = x \to 1^{st} (G) (p) = 1^{st} (G) (x)$
54		fveq2	$⊢ p = x \to 1^{st} (L) (p) = 1^{st} (L) (x)$
55	53 54	opeq12d	$⊢ p = x \to ⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ = ⟨1^{st} (G) (x), 1^{st} (L) (x)⟩$
56		fveq2	$⊢ p = x \to 1^{st} (N) (p) = 1^{st} (N) (x)$
57	55 56	oveq12d	$⊢ p = x \to ⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p) = ⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{} 1^{st} (N) (x)$
58		fveq2	$⊢ p = x \to V (p) = V (x)$
59		fveq2	$⊢ p = x \to S (p) = S (x)$
60	57 58 59	oveq123d	$⊢ p = x \to V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p) = V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{} 1^{st} (N) (x)) S (x)$
61		eqid	$⊢ (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) = (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p))$
62		ovex	$⊢ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{*} 1^{st} (N) (p)) S (p) \in V$
63	60 61 62	fvmpt3i	$⊢ x \in {Base}_{C} \to (p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) (x) = V (x) (⟨1^{st} (G) (x), 1^{st} (L) (x)⟩ \underset{˙}{} 1^{st} (N) (x)) S (x)$
64	63	fveq2d	$⊢ x \in {Base}_{C} \to (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) ((p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) (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))$
65	64	adantl	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (G) (x) 2^{nd} (F) 1^{st} (N) (x)) ((p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) (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))$
66	52 65	oveq12d	$⊢ (φ \land x \in {Base}_{C}) \to (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) (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)) ((p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) (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} (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))$
67	66	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ (p \in {Base}_{D} ⟼ U (p) (⟨1^{st} (F) (p), 1^{st} (K) (p)⟩ comp (E) 1^{st} (M) (p)) R (p)) (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)) ((p \in {Base}_{C} ⟼ V (p) (⟨1^{st} (G) (p), 1^{st} (L) (p)⟩ \underset{˙}{} 1^{st} (N) (p)) S (p)) (x))) = (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)))$
68	24 31 67	3eqtrd	$⊢ φ \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)))$

Metamath Proof Explorer

Theorem fucocolem2

Proof