Metamath Proof Explorer

Theorem fucoco2

Description: Composition in the source category is mapped to composition in the target. See also fucoco . (Contributed by Zhi Wang, 3-Oct-2025)

Ref Expression
Hypotheses fucoco2.t 
|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
fucoco2.q 
|- Q = ( C FuncCat E )
fucoco2.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fucoco2.1 
|- .x. = ( comp ` T )
fucoco2.2 
|- .xb = ( comp ` Q )
fucoco2.w 
|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
fucoco2.x 
|- ( ph -> X e. W )
fucoco2.y 
|- ( ph -> Y e. W )
fucoco2.z 
|- ( ph -> Z e. W )
fucoco2.j 
|- J = ( Hom ` T )
fucoco2.a 
|- ( ph -> A e. ( X J Y ) )
fucoco2.b 
|- ( ph -> B e. ( Y J Z ) )
Assertion fucoco2 
|- ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( ( ( Y P Z ) ` B ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 fucoco2.t 
 |-  T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
2 fucoco2.q 
 |-  Q = ( C FuncCat E )
3 fucoco2.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
4 fucoco2.1 
 |-  .x. = ( comp ` T )
5 fucoco2.2 
 |-  .xb = ( comp ` Q )
6 fucoco2.w 
 |-  ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
7 fucoco2.x 
 |-  ( ph -> X e. W )
8 fucoco2.y 
 |-  ( ph -> Y e. W )
9 fucoco2.z 
 |-  ( ph -> Z e. W )
10 fucoco2.j 
 |-  J = ( Hom ` T )
11 fucoco2.a 
 |-  ( ph -> A e. ( X J Y ) )
12 fucoco2.b 
 |-  ( ph -> B e. ( Y J Z ) )
13 1 xpcfucbas 
 |-  ( ( D Func E ) X. ( C Func D ) ) = ( Base ` T )
14 7 6 eleqtrd 
 |-  ( ph -> X e. ( ( D Func E ) X. ( C Func D ) ) )
15 8 6 eleqtrd 
 |-  ( ph -> Y e. ( ( D Func E ) X. ( C Func D ) ) )
16 1 13 10 14 15 xpcfuchom 
 |-  ( ph -> ( X J Y ) = ( ( ( 1st ` X ) ( D Nat E ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( C Nat D ) ( 2nd ` Y ) ) ) )
17 11 16 eleqtrd 
 |-  ( ph -> A e. ( ( ( 1st ` X ) ( D Nat E ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( C Nat D ) ( 2nd ` Y ) ) ) )
18 xp1st 
 |-  ( A e. ( ( ( 1st ` X ) ( D Nat E ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( C Nat D ) ( 2nd ` Y ) ) ) -> ( 1st ` A ) e. ( ( 1st ` X ) ( D Nat E ) ( 1st ` Y ) ) )
19 17 18 syl 
 |-  ( ph -> ( 1st ` A ) e. ( ( 1st ` X ) ( D Nat E ) ( 1st ` Y ) ) )
20 xp2nd 
 |-  ( A e. ( ( ( 1st ` X ) ( D Nat E ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( C Nat D ) ( 2nd ` Y ) ) ) -> ( 2nd ` A ) e. ( ( 2nd ` X ) ( C Nat D ) ( 2nd ` Y ) ) )
21 17 20 syl 
 |-  ( ph -> ( 2nd ` A ) e. ( ( 2nd ` X ) ( C Nat D ) ( 2nd ` Y ) ) )
22 9 6 eleqtrd 
 |-  ( ph -> Z e. ( ( D Func E ) X. ( C Func D ) ) )
23 1 13 10 15 22 xpcfuchom 
 |-  ( ph -> ( Y J Z ) = ( ( ( 1st ` Y ) ( D Nat E ) ( 1st ` Z ) ) X. ( ( 2nd ` Y ) ( C Nat D ) ( 2nd ` Z ) ) ) )
24 12 23 eleqtrd 
 |-  ( ph -> B e. ( ( ( 1st ` Y ) ( D Nat E ) ( 1st ` Z ) ) X. ( ( 2nd ` Y ) ( C Nat D ) ( 2nd ` Z ) ) ) )
25 xp1st 
 |-  ( B e. ( ( ( 1st ` Y ) ( D Nat E ) ( 1st ` Z ) ) X. ( ( 2nd ` Y ) ( C Nat D ) ( 2nd ` Z ) ) ) -> ( 1st ` B ) e. ( ( 1st ` Y ) ( D Nat E ) ( 1st ` Z ) ) )
26 24 25 syl 
 |-  ( ph -> ( 1st ` B ) e. ( ( 1st ` Y ) ( D Nat E ) ( 1st ` Z ) ) )
27 xp2nd 
 |-  ( B e. ( ( ( 1st ` Y ) ( D Nat E ) ( 1st ` Z ) ) X. ( ( 2nd ` Y ) ( C Nat D ) ( 2nd ` Z ) ) ) -> ( 2nd ` B ) e. ( ( 2nd ` Y ) ( C Nat D ) ( 2nd ` Z ) ) )
28 24 27 syl 
 |-  ( ph -> ( 2nd ` B ) e. ( ( 2nd ` Y ) ( C Nat D ) ( 2nd ` Z ) ) )
29 1st2nd2 
 |-  ( X e. ( ( D Func E ) X. ( C Func D ) ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
30 14 29 syl 
 |-  ( ph -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
31 1st2nd2 
 |-  ( Y e. ( ( D Func E ) X. ( C Func D ) ) -> Y = <. ( 1st ` Y ) , ( 2nd ` Y ) >. )
32 15 31 syl 
 |-  ( ph -> Y = <. ( 1st ` Y ) , ( 2nd ` Y ) >. )
33 1st2nd2 
 |-  ( Z e. ( ( D Func E ) X. ( C Func D ) ) -> Z = <. ( 1st ` Z ) , ( 2nd ` Z ) >. )
34 22 33 syl 
 |-  ( ph -> Z = <. ( 1st ` Z ) , ( 2nd ` Z ) >. )
35 1st2nd2 
 |-  ( A e. ( ( ( 1st ` X ) ( D Nat E ) ( 1st ` Y ) ) X. ( ( 2nd ` X ) ( C Nat D ) ( 2nd ` Y ) ) ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
36 17 35 syl 
 |-  ( ph -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
37 1st2nd2 
 |-  ( B e. ( ( ( 1st ` Y ) ( D Nat E ) ( 1st ` Z ) ) X. ( ( 2nd ` Y ) ( C Nat D ) ( 2nd ` Z ) ) ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
38 24 37 syl 
 |-  ( ph -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
39 19 21 26 28 3 30 32 34 36 38 2 5 1 4 fucoco 
 |-  ( ph -> ( ( X P Z ) ` ( B ( <. X , Y >. .x. Z ) A ) ) = ( ( ( Y P Z ) ` B ) ( <. ( O ` X ) , ( O ` Y ) >. .xb ( O ` Z ) ) ( ( X P Y ) ` A ) ) )