fuco22natlem1

Description: Lemma for fuco22nat . The commutative square of natural transformation A in category D , mapped to category E by the morphism part L of the functor. (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fuco22natlem1.x	$⊢ φ \to X \in {Base}_{C}$
	fuco22natlem1.y	$⊢ φ \to Y \in {Base}_{C}$
	fuco22natlem1.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
	fuco22natlem1.h	$⊢ φ \to H \in (X Hom (C) Y)$
	fuco22natlem1.k	$⊢ φ \to K (D Func E) L$
Assertion	fuco22natlem1	$⊢ φ \to (F (Y) L M (Y)) (A (Y)) (⟨K (F (X)), K (F (Y))⟩ comp (E) K (M (Y))) (F (X) L F (Y)) ((X G Y) (H)) = (M (X) L M (Y)) ((X N Y) (H)) (⟨K (F (X)), K (M (X))⟩ comp (E) K (M (Y))) (F (X) L M (X)) (A (X))$

Proof

Step	Hyp	Ref	Expression
1		fuco22natlem1.x	$⊢ φ \to X \in {Base}_{C}$
2		fuco22natlem1.y	$⊢ φ \to Y \in {Base}_{C}$
3		fuco22natlem1.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
4		fuco22natlem1.h	$⊢ φ \to H \in (X Hom (C) Y)$
5		fuco22natlem1.k	$⊢ φ \to K (D Func E) L$
6		eqid	$⊢ C Nat D = C Nat D$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (D) = comp (D)$
10	6 3 7 8 9 1 2 4	nati	$⊢ φ \to A (Y) (⟨F (X), F (Y)⟩ comp (D) M (Y)) (X G Y) (H) = (X N Y) (H) (⟨F (X), M (X)⟩ comp (D) M (Y)) A (X)$
11	10	fveq2d	$⊢ φ \to (F (X) L M (Y)) (A (Y) (⟨F (X), F (Y)⟩ comp (D) M (Y)) (X G Y) (H)) = (F (X) L M (Y)) ((X N Y) (H) (⟨F (X), M (X)⟩ comp (D) M (Y)) A (X))$
12		eqid	$⊢ {Base}_{D} = {Base}_{D}$
13		eqid	$⊢ Hom (D) = Hom (D)$
14		eqid	$⊢ comp (E) = comp (E)$
15	6 3	natrcl2	$⊢ φ \to F (C Func D) G$
16	7 12 15	funcf1	$⊢ φ \to F : {Base}_{C} ⟶ {Base}_{D}$
17	16 1	ffvelcdmd	$⊢ φ \to F (X) \in {Base}_{D}$
18	16 2	ffvelcdmd	$⊢ φ \to F (Y) \in {Base}_{D}$
19	6 3	natrcl3	$⊢ φ \to M (C Func D) N$
20	7 12 19	funcf1	$⊢ φ \to M : {Base}_{C} ⟶ {Base}_{D}$
21	20 2	ffvelcdmd	$⊢ φ \to M (Y) \in {Base}_{D}$
22	7 8 13 15 1 2	funcf2	$⊢ φ \to (X G Y) : X Hom (C) Y ⟶ F (X) Hom (D) F (Y)$
23	22 4	ffvelcdmd	$⊢ φ \to (X G Y) (H) \in (F (X) Hom (D) F (Y))$
24	6 3 7 13 2	natcl	$⊢ φ \to A (Y) \in (F (Y) Hom (D) M (Y))$
25	12 13 9 14 5 17 18 21 23 24	funcco	$⊢ φ \to (F (X) L M (Y)) (A (Y) (⟨F (X), F (Y)⟩ comp (D) M (Y)) (X G Y) (H)) = (F (Y) L M (Y)) (A (Y)) (⟨K (F (X)), K (F (Y))⟩ comp (E) K (M (Y))) (F (X) L F (Y)) ((X G Y) (H))$
26	20 1	ffvelcdmd	$⊢ φ \to M (X) \in {Base}_{D}$
27	6 3 7 13 1	natcl	$⊢ φ \to A (X) \in (F (X) Hom (D) M (X))$
28	7 8 13 19 1 2	funcf2	$⊢ φ \to (X N Y) : X Hom (C) Y ⟶ M (X) Hom (D) M (Y)$
29	28 4	ffvelcdmd	$⊢ φ \to (X N Y) (H) \in (M (X) Hom (D) M (Y))$
30	12 13 9 14 5 17 26 21 27 29	funcco	$⊢ φ \to (F (X) L M (Y)) ((X N Y) (H) (⟨F (X), M (X)⟩ comp (D) M (Y)) A (X)) = (M (X) L M (Y)) ((X N Y) (H)) (⟨K (F (X)), K (M (X))⟩ comp (E) K (M (Y))) (F (X) L M (X)) (A (X))$
31	11 25 30	3eqtr3d	$⊢ φ \to (F (Y) L M (Y)) (A (Y)) (⟨K (F (X)), K (F (Y))⟩ comp (E) K (M (Y))) (F (X) L F (Y)) ((X G Y) (H)) = (M (X) L M (Y)) ((X N Y) (H)) (⟨K (F (X)), K (M (X))⟩ comp (E) K (M (Y))) (F (X) L M (X)) (A (X))$

Metamath Proof Explorer

Theorem fuco22natlem1

Proof