This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cofu2a

Description: Value of the morphism part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025)

Ref Expression
Hypotheses cofu1a.b 
|- B = ( Base ` C )
cofu1a.f 
|- ( ph -> F ( C Func D ) G )
cofu1a.k 
|- ( ph -> K ( D Func E ) L )
cofu1a.m 
|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = <. M , N >. )
cofu1a.x 
|- ( ph -> X e. B )
cofu2a.y 
|- ( ph -> Y e. B )
cofu2a.h 
|- H = ( Hom ` C )
cofu2a.r 
|- ( ph -> R e. ( X H Y ) )
Assertion cofu2a 
|- ( ph -> ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( X N Y ) ` R ) )

Proof

Step Hyp Ref Expression
1 cofu1a.b 
 |-  B = ( Base ` C )
2 cofu1a.f 
 |-  ( ph -> F ( C Func D ) G )
3 cofu1a.k 
 |-  ( ph -> K ( D Func E ) L )
4 cofu1a.m 
 |-  ( ph -> ( <. K , L >. o.func <. F , G >. ) = <. M , N >. )
5 cofu1a.x 
 |-  ( ph -> X e. B )
6 cofu2a.y 
 |-  ( ph -> Y e. B )
7 cofu2a.h 
 |-  H = ( Hom ` C )
8 cofu2a.r 
 |-  ( ph -> R e. ( X H Y ) )
9 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
10 2 9 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
11 df-br 
 |-  ( K ( D Func E ) L <-> <. K , L >. e. ( D Func E ) )
12 3 11 sylib 
 |-  ( ph -> <. K , L >. e. ( D Func E ) )
13 1 10 12 5 6 7 8 cofu2 
 |-  ( ph -> ( ( X ( 2nd ` ( <. K , L >. o.func <. F , G >. ) ) Y ) ` R ) = ( ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) ` ( ( X ( 2nd ` <. F , G >. ) Y ) ` R ) ) )
14 4 fveq2d 
 |-  ( ph -> ( 2nd ` ( <. K , L >. o.func <. F , G >. ) ) = ( 2nd ` <. M , N >. ) )
15 10 12 cofucl 
 |-  ( ph -> ( <. K , L >. o.func <. F , G >. ) e. ( C Func E ) )
16 4 15 eqeltrrd 
 |-  ( ph -> <. M , N >. e. ( C Func E ) )
17 df-br 
 |-  ( M ( C Func E ) N <-> <. M , N >. e. ( C Func E ) )
18 16 17 sylibr 
 |-  ( ph -> M ( C Func E ) N )
19 18 func2nd 
 |-  ( ph -> ( 2nd ` <. M , N >. ) = N )
20 14 19 eqtrd 
 |-  ( ph -> ( 2nd ` ( <. K , L >. o.func <. F , G >. ) ) = N )
21 20 oveqd 
 |-  ( ph -> ( X ( 2nd ` ( <. K , L >. o.func <. F , G >. ) ) Y ) = ( X N Y ) )
22 21 fveq1d 
 |-  ( ph -> ( ( X ( 2nd ` ( <. K , L >. o.func <. F , G >. ) ) Y ) ` R ) = ( ( X N Y ) ` R ) )
23 3 func2nd 
 |-  ( ph -> ( 2nd ` <. K , L >. ) = L )
24 2 func1st 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
25 24 fveq1d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) ` X ) = ( F ` X ) )
26 24 fveq1d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) ` Y ) = ( F ` Y ) )
27 23 25 26 oveq123d 
 |-  ( ph -> ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) = ( ( F ` X ) L ( F ` Y ) ) )
28 2 func2nd 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
29 28 oveqd 
 |-  ( ph -> ( X ( 2nd ` <. F , G >. ) Y ) = ( X G Y ) )
30 29 fveq1d 
 |-  ( ph -> ( ( X ( 2nd ` <. F , G >. ) Y ) ` R ) = ( ( X G Y ) ` R ) )
31 27 30 fveq12d 
 |-  ( ph -> ( ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) ` ( ( X ( 2nd ` <. F , G >. ) Y ) ` R ) ) = ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) )
32 13 22 31 3eqtr3rd 
 |-  ( ph -> ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( X N Y ) ` R ) )