Metamath Proof Explorer

Theorem cofid2

Description: Express the morphism part of ( G o.func F ) = I explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Hypotheses cofid1a.i 
|- I = ( idFunc ` D )
cofid1a.b 
|- B = ( Base ` D )
cofid1a.x 
|- ( ph -> X e. B )
cofid1.f 
|- ( ph -> F ( D Func E ) G )
cofid1.k 
|- ( ph -> K ( E Func D ) L )
cofid1.o 
|- ( ph -> ( <. K , L >. o.func <. F , G >. ) = I )
cofid2.y 
|- ( ph -> Y e. B )
cofid2.h 
|- H = ( Hom ` D )
cofid2.r 
|- ( ph -> R e. ( X H Y ) )
Assertion cofid2 
|- ( ph -> ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = R )

Proof

Step Hyp Ref Expression
1 cofid1a.i 
 |-  I = ( idFunc ` D )
2 cofid1a.b 
 |-  B = ( Base ` D )
3 cofid1a.x 
 |-  ( ph -> X e. B )
4 cofid1.f 
 |-  ( ph -> F ( D Func E ) G )
5 cofid1.k 
 |-  ( ph -> K ( E Func D ) L )
6 cofid1.o 
 |-  ( ph -> ( <. K , L >. o.func <. F , G >. ) = I )
7 cofid2.y 
 |-  ( ph -> Y e. B )
8 cofid2.h 
 |-  H = ( Hom ` D )
9 cofid2.r 
 |-  ( ph -> R e. ( X H Y ) )
10 5 func2nd 
 |-  ( ph -> ( 2nd ` <. K , L >. ) = L )
11 4 func1st 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
12 11 fveq1d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) ` X ) = ( F ` X ) )
13 11 fveq1d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) ` Y ) = ( F ` Y ) )
14 10 12 13 oveq123d 
 |-  ( ph -> ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) = ( ( F ` X ) L ( F ` Y ) ) )
15 4 func2nd 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
16 15 oveqd 
 |-  ( ph -> ( X ( 2nd ` <. F , G >. ) Y ) = ( X G Y ) )
17 16 fveq1d 
 |-  ( ph -> ( ( X ( 2nd ` <. F , G >. ) Y ) ` R ) = ( ( X G Y ) ` R ) )
18 14 17 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 ) ) )
19 df-br 
 |-  ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
20 4 19 sylib 
 |-  ( ph -> <. F , G >. e. ( D Func E ) )
21 df-br 
 |-  ( K ( E Func D ) L <-> <. K , L >. e. ( E Func D ) )
22 5 21 sylib 
 |-  ( ph -> <. K , L >. e. ( E Func D ) )
23 1 2 3 20 22 6 7 8 9 cofid2a 
 |-  ( ph -> ( ( ( ( 1st ` <. F , G >. ) ` X ) ( 2nd ` <. K , L >. ) ( ( 1st ` <. F , G >. ) ` Y ) ) ` ( ( X ( 2nd ` <. F , G >. ) Y ) ` R ) ) = R )
24 18 23 eqtr3d 
 |-  ( ph -> ( ( ( F ` X ) L ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = R )