Metamath Proof Explorer

Theorem 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 
|- ( 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 ) )
fuco22natlem1.k 
|- ( ph -> K ( D Func E ) L )
Assertion 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 ) ) ) )

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 fuco22natlem1.k 
 |-  ( ph -> 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 
 |-  ( ph -> ( ( 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 
 |-  ( ph -> ( ( ( 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 
 |-  ( ph -> F ( C Func D ) G )
16 7 12 15 funcf1 
 |-  ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
17 16 1 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. ( Base ` D ) )
18 16 2 ffvelcdmd 
 |-  ( ph -> ( F ` Y ) e. ( Base ` D ) )
19 6 3 natrcl3 
 |-  ( ph -> M ( C Func D ) N )
20 7 12 19 funcf1 
 |-  ( ph -> M : ( Base ` C ) --> ( Base ` D ) )
21 20 2 ffvelcdmd 
 |-  ( ph -> ( M ` Y ) e. ( Base ` D ) )
22 7 8 13 15 1 2 funcf2 
 |-  ( ph -> ( X G Y ) : ( X ( Hom ` C ) Y ) --> ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) )
23 22 4 ffvelcdmd 
 |-  ( ph -> ( ( X G Y ) ` H ) e. ( ( F ` X ) ( Hom ` D ) ( F ` Y ) ) )
24 6 3 7 13 2 natcl 
 |-  ( ph -> ( A ` Y ) e. ( ( F ` Y ) ( Hom ` D ) ( M ` Y ) ) )
25 12 13 9 14 5 17 18 21 23 24 funcco 
 |-  ( ph -> ( ( ( 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 
 |-  ( ph -> ( M ` X ) e. ( Base ` D ) )
27 6 3 7 13 1 natcl 
 |-  ( ph -> ( A ` X ) e. ( ( F ` X ) ( Hom ` D ) ( M ` X ) ) )
28 7 8 13 19 1 2 funcf2 
 |-  ( ph -> ( X N Y ) : ( X ( Hom ` C ) Y ) --> ( ( M ` X ) ( Hom ` D ) ( M ` Y ) ) )
29 28 4 ffvelcdmd 
 |-  ( ph -> ( ( X N Y ) ` H ) e. ( ( M ` X ) ( Hom ` D ) ( M ` Y ) ) )
30 12 13 9 14 5 17 26 21 27 29 funcco 
 |-  ( ph -> ( ( ( 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 
 |-  ( 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 ) ) ) )