Metamath Proof Explorer

Theorem xpcfucco3

Description: Value of composition in the binary product of categories of functors; expressed explicitly. (Contributed by Zhi Wang, 1-Oct-2025)

Ref Expression
Hypotheses xpcfuchom2.t 
|- T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
xpcfucco2.o 
|- O = ( comp ` T )
xpcfucco2.f 
|- ( ph -> F e. ( M ( B Nat C ) P ) )
xpcfucco2.g 
|- ( ph -> G e. ( N ( D Nat E ) Q ) )
xpcfucco2.k 
|- ( ph -> K e. ( P ( B Nat C ) R ) )
xpcfucco2.l 
|- ( ph -> L e. ( Q ( D Nat E ) S ) )
xpcfucco3.x 
|- X = ( Base ` B )
xpcfucco3.y 
|- Y = ( Base ` D )
xpcfucco3.o1 
|- .x. = ( comp ` C )
xpcfucco3.o2 
|- .xb = ( comp ` E )
Assertion xpcfucco3 
|- ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( x e. X |-> ( ( K ` x ) ( <. ( ( 1st ` M ) ` x ) , ( ( 1st ` P ) ` x ) >. .x. ( ( 1st ` R ) ` x ) ) ( F ` x ) ) ) , ( y e. Y |-> ( ( L ` y ) ( <. ( ( 1st ` N ) ` y ) , ( ( 1st ` Q ) ` y ) >. .xb ( ( 1st ` S ) ` y ) ) ( G ` y ) ) ) >. )

Proof

Step Hyp Ref Expression
1 xpcfuchom2.t 
 |-  T = ( ( B FuncCat C ) Xc. ( D FuncCat E ) )
2 xpcfucco2.o 
 |-  O = ( comp ` T )
3 xpcfucco2.f 
 |-  ( ph -> F e. ( M ( B Nat C ) P ) )
4 xpcfucco2.g 
 |-  ( ph -> G e. ( N ( D Nat E ) Q ) )
5 xpcfucco2.k 
 |-  ( ph -> K e. ( P ( B Nat C ) R ) )
6 xpcfucco2.l 
 |-  ( ph -> L e. ( Q ( D Nat E ) S ) )
7 xpcfucco3.x 
 |-  X = ( Base ` B )
8 xpcfucco3.y 
 |-  Y = ( Base ` D )
9 xpcfucco3.o1 
 |-  .x. = ( comp ` C )
10 xpcfucco3.o2 
 |-  .xb = ( comp ` E )
11 1 2 3 4 5 6 xpcfucco2 
 |-  ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( K ( <. M , P >. ( comp ` ( B FuncCat C ) ) R ) F ) , ( L ( <. N , Q >. ( comp ` ( D FuncCat E ) ) S ) G ) >. )
12 eqid 
 |-  ( B FuncCat C ) = ( B FuncCat C )
13 eqid 
 |-  ( B Nat C ) = ( B Nat C )
14 eqid 
 |-  ( comp ` ( B FuncCat C ) ) = ( comp ` ( B FuncCat C ) )
15 12 13 7 9 14 3 5 fucco 
 |-  ( ph -> ( K ( <. M , P >. ( comp ` ( B FuncCat C ) ) R ) F ) = ( x e. X |-> ( ( K ` x ) ( <. ( ( 1st ` M ) ` x ) , ( ( 1st ` P ) ` x ) >. .x. ( ( 1st ` R ) ` x ) ) ( F ` x ) ) ) )
16 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
17 eqid 
 |-  ( D Nat E ) = ( D Nat E )
18 eqid 
 |-  ( comp ` ( D FuncCat E ) ) = ( comp ` ( D FuncCat E ) )
19 16 17 8 10 18 4 6 fucco 
 |-  ( ph -> ( L ( <. N , Q >. ( comp ` ( D FuncCat E ) ) S ) G ) = ( y e. Y |-> ( ( L ` y ) ( <. ( ( 1st ` N ) ` y ) , ( ( 1st ` Q ) ` y ) >. .xb ( ( 1st ` S ) ` y ) ) ( G ` y ) ) ) )
20 15 19 opeq12d 
 |-  ( ph -> <. ( K ( <. M , P >. ( comp ` ( B FuncCat C ) ) R ) F ) , ( L ( <. N , Q >. ( comp ` ( D FuncCat E ) ) S ) G ) >. = <. ( x e. X |-> ( ( K ` x ) ( <. ( ( 1st ` M ) ` x ) , ( ( 1st ` P ) ` x ) >. .x. ( ( 1st ` R ) ` x ) ) ( F ` x ) ) ) , ( y e. Y |-> ( ( L ` y ) ( <. ( ( 1st ` N ) ` y ) , ( ( 1st ` Q ) ` y ) >. .xb ( ( 1st ` S ) ` y ) ) ( G ` y ) ) ) >. )
21 11 20 eqtrd 
 |-  ( ph -> ( <. K , L >. ( <. <. M , N >. , <. P , Q >. >. O <. R , S >. ) <. F , G >. ) = <. ( x e. X |-> ( ( K ` x ) ( <. ( ( 1st ` M ) ` x ) , ( ( 1st ` P ) ` x ) >. .x. ( ( 1st ` R ) ` x ) ) ( F ` x ) ) ) , ( y e. Y |-> ( ( L ` y ) ( <. ( ( 1st ` N ) ` y ) , ( ( 1st ` Q ) ` y ) >. .xb ( ( 1st ` S ) ` y ) ) ( G ` y ) ) ) >. )