Theorem fuco22natlem2

Description: Lemma for fuco22nat . The commutative square of natural transformation B in category E , combined with the commutative square of fuco22natlem1 . (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fuco22natlem1.x	|- ( ph -> X e. ( Base ` C ) )
	fuco22natlem1.y	|- ( ph -> Y e. ( Base ` C ) )
	fuco22natlem1.a	|- ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
	fuco22natlem1.h	|- ( ph -> H e. ( X ( Hom ` C ) Y ) )
	fuco22natlem2.b	|- ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
Assertion	fuco22natlem2	|- ( ph -> ( ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` Y ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` Y ) L ( M ` Y ) ) ` ( A ` Y ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( F ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` H ) ) ) = ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco22natlem1.x	|- ( ph -> X e. ( Base ` C ) )
2		fuco22natlem1.y	|- ( ph -> Y e. ( Base ` C ) )
3		fuco22natlem1.a	|- ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
4		fuco22natlem1.h	|- ( ph -> H e. ( X ( Hom ` C ) Y ) )
5		fuco22natlem2.b	|- ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
6		eqid	|- ( Base ` E ) = ( Base ` E )
7		eqid	|- ( Hom ` E ) = ( Hom ` E )
8		eqid	|- ( comp ` E ) = ( comp ` E )
9		eqid	|- ( D Nat E ) = ( D Nat E )
10	9 5	natrcl2	|- ( ph -> K ( D Func E ) L )
11	10	funcrcl3	|- ( ph -> E e. Cat )
12		eqid	|- ( Base ` D ) = ( Base ` D )
13	12 6 10	funcf1	|- ( ph -> K : ( Base ` D ) --> ( Base ` E ) )
14		eqid	|- ( Base ` C ) = ( Base ` C )
15		eqid	|- ( C Nat D ) = ( C Nat D )
16	15 3	natrcl2	|- ( ph -> F ( C Func D ) G )
17	14 12 16	funcf1	|- ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
18	17 1	ffvelcdmd	|- ( ph -> ( F ` X ) e. ( Base ` D ) )
19	13 18	ffvelcdmd	|- ( ph -> ( K ` ( F ` X ) ) e. ( Base ` E ) )
20	17 2	ffvelcdmd	|- ( ph -> ( F ` Y ) e. ( Base ` D ) )
21	13 20	ffvelcdmd	|- ( ph -> ( K ` ( F ` Y ) ) e. ( Base ` E ) )
22	15 3	natrcl3	|- ( ph -> M ( C Func D ) N )
23	14 12 22	funcf1	|- ( ph -> M : ( Base ` C ) --> ( Base ` D ) )
24	23 2	ffvelcdmd	|- ( ph -> ( M ` Y ) e. ( Base ` D ) )
25	13 24	ffvelcdmd	|- ( ph -> ( K ` ( M ` Y ) ) e. ( Base ` E ) )
26		eqid	|- ( Hom ` D ) = ( Hom ` D )
27	12 26 7 10 18 20	funcf2	|- ( ph -> ( ( F ` X ) L ( F ` Y ) ) : ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) --> ( ( K ` ( F ` X ) ) ( Hom ` E ) ( K ` ( F ` Y ) ) ) )
28		eqid	|- ( Hom ` C ) = ( Hom ` C )
29	14 28 26 16 1 2	funcf2	|- ( ph -> ( X G Y ) : ( X ( Hom ` C ) Y ) --> ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) )
30	29 4	ffvelcdmd	|- ( ph -> ( ( X G Y ) ` H ) e. ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) )
31	27 30	ffvelcdmd	|- ( ph -> ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` H ) ) e. ( ( K ` ( F ` X ) ) ( Hom ` E ) ( K ` ( F ` Y ) ) ) )
32	12 26 7 10 20 24	funcf2	|- ( ph -> ( ( F ` Y ) L ( M ` Y ) ) : ( ( F ` Y ) ( Hom ` D ) ( M ` Y ) ) --> ( ( K ` ( F ` Y ) ) ( Hom ` E ) ( K ` ( M ` Y ) ) ) )
33	15 3 14 26 2	natcl	|- ( ph -> ( A ` Y ) e. ( ( F ` Y ) ( Hom ` D ) ( M ` Y ) ) )
34	32 33	ffvelcdmd	|- ( ph -> ( ( ( F ` Y ) L ( M ` Y ) ) ` ( A ` Y ) ) e. ( ( K ` ( F ` Y ) ) ( Hom ` E ) ( K ` ( M ` Y ) ) ) )
35	9 5	natrcl3	|- ( ph -> R ( D Func E ) S )
36	12 6 35	funcf1	|- ( ph -> R : ( Base ` D ) --> ( Base ` E ) )
37	36 24	ffvelcdmd	|- ( ph -> ( R ` ( M ` Y ) ) e. ( Base ` E ) )
38	9 5 12 7 24	natcl	|- ( ph -> ( B ` ( M ` Y ) ) e. ( ( K ` ( M ` Y ) ) ( Hom ` E ) ( R ` ( M ` Y ) ) ) )
39	6 7 8 11 19 21 25 31 34 37 38	catass	|- ( ph -> ( ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` Y ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` Y ) L ( M ` Y ) ) ` ( A ` Y ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( F ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` H ) ) ) = ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( ( 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 ) ) ) ) )
40	1 2 3 4 10	fuco22natlem1	|- ( ph -> ( ( ( ( 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 ) ) ) )
41	40	oveq2d	|- ( ph -> ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( ( 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 ) ) ) ) = ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( ( 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 ) ) ) ) )
42	23 1	ffvelcdmd	|- ( ph -> ( M ` X ) e. ( Base ` D ) )
43	14 28 26 22 1 2	funcf2	|- ( ph -> ( X N Y ) : ( X ( Hom ` C ) Y ) --> ( ( M ` X ) ( Hom ` D ) ( M ` Y ) ) )
44	43 4	ffvelcdmd	|- ( ph -> ( ( X N Y ) ` H ) e. ( ( M ` X ) ( Hom ` D ) ( M ` Y ) ) )
45	9 5 12 26 8 42 24 44	nati	|- ( ph -> ( ( B ` ( M ` Y ) ) ( <. ( K ` ( M ` X ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( M ` X ) L ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ) = ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( M ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( B ` ( M ` X ) ) ) )
46	45	oveq1d	|- ( ph -> ( ( ( B ` ( M ` Y ) ) ( <. ( K ` ( M ` X ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( M ` X ) L ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) = ( ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( M ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( B ` ( M ` X ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) )
47	13 42	ffvelcdmd	|- ( ph -> ( K ` ( M ` X ) ) e. ( Base ` E ) )
48	12 26 7 10 18 42	funcf2	|- ( ph -> ( ( F ` X ) L ( M ` X ) ) : ( ( F ` X ) ( Hom ` D ) ( M ` X ) ) --> ( ( K ` ( F ` X ) ) ( Hom ` E ) ( K ` ( M ` X ) ) ) )
49	15 3 14 26 1	natcl	|- ( ph -> ( A ` X ) e. ( ( F ` X ) ( Hom ` D ) ( M ` X ) ) )
50	48 49	ffvelcdmd	|- ( ph -> ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) e. ( ( K ` ( F ` X ) ) ( Hom ` E ) ( K ` ( M ` X ) ) ) )
51	12 26 7 10 42 24	funcf2	|- ( ph -> ( ( M ` X ) L ( M ` Y ) ) : ( ( M ` X ) ( Hom ` D ) ( M ` Y ) ) --> ( ( K ` ( M ` X ) ) ( Hom ` E ) ( K ` ( M ` Y ) ) ) )
52	51 44	ffvelcdmd	|- ( ph -> ( ( ( M ` X ) L ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) e. ( ( K ` ( M ` X ) ) ( Hom ` E ) ( K ` ( M ` Y ) ) ) )
53	6 7 8 11 19 47 25 50 52 37 38	catass	|- ( ph -> ( ( ( B ` ( M ` Y ) ) ( <. ( K ` ( M ` X ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( M ` X ) L ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) = ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( ( 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 ) ) ) ) )
54	36 42	ffvelcdmd	|- ( ph -> ( R ` ( M ` X ) ) e. ( Base ` E ) )
55	9 5 12 7 42	natcl	|- ( ph -> ( B ` ( M ` X ) ) e. ( ( K ` ( M ` X ) ) ( Hom ` E ) ( R ` ( M ` X ) ) ) )
56	12 26 7 35 42 24	funcf2	|- ( ph -> ( ( M ` X ) S ( M ` Y ) ) : ( ( M ` X ) ( Hom ` D ) ( M ` Y ) ) --> ( ( R ` ( M ` X ) ) ( Hom ` E ) ( R ` ( M ` Y ) ) ) )
57	56 44	ffvelcdmd	|- ( ph -> ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) e. ( ( R ` ( M ` X ) ) ( Hom ` E ) ( R ` ( M ` Y ) ) ) )
58	6 7 8 11 19 47 54 50 55 37 57	catass	|- ( ph -> ( ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( M ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( B ` ( M ` X ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) = ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) ) )
59	46 53 58	3eqtr3d	|- ( ph -> ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( ( 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 ) ) ) ) = ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) ) )
60	39 41 59	3eqtrd	|- ( ph -> ( ( ( B ` ( M ` Y ) ) ( <. ( K ` ( F ` Y ) ) , ( K ` ( M ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` Y ) L ( M ` Y ) ) ` ( A ` Y ) ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( F ` Y ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` H ) ) ) = ( ( ( ( M ` X ) S ( M ` Y ) ) ` ( ( X N Y ) ` H ) ) ( <. ( K ` ( F ` X ) ) , ( R ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` Y ) ) ) ( ( B ` ( M ` X ) ) ( <. ( K ` ( F ` X ) ) , ( K ` ( M ` X ) ) >. ( comp ` E ) ( R ` ( M ` X ) ) ) ( ( ( F ` X ) L ( M ` X ) ) ` ( A ` X ) ) ) ) )