Metamath Proof Explorer


Theorem cofu2

Description: Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses cofuval.b
|- B = ( Base ` C )
cofuval.f
|- ( ph -> F e. ( C Func D ) )
cofuval.g
|- ( ph -> G e. ( D Func E ) )
cofu2nd.x
|- ( ph -> X e. B )
cofu2nd.y
|- ( ph -> Y e. B )
cofu2.h
|- H = ( Hom ` C )
cofu2.y
|- ( ph -> R e. ( X H Y ) )
Assertion cofu2
|- ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) )

Proof

Step Hyp Ref Expression
1 cofuval.b
 |-  B = ( Base ` C )
2 cofuval.f
 |-  ( ph -> F e. ( C Func D ) )
3 cofuval.g
 |-  ( ph -> G e. ( D Func E ) )
4 cofu2nd.x
 |-  ( ph -> X e. B )
5 cofu2nd.y
 |-  ( ph -> Y e. B )
6 cofu2.h
 |-  H = ( Hom ` C )
7 cofu2.y
 |-  ( ph -> R e. ( X H Y ) )
8 1 2 3 4 5 cofu2nd
 |-  ( ph -> ( X ( 2nd ` ( G o.func F ) ) Y ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) )
9 8 fveq1d
 |-  ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) ` R ) )
10 eqid
 |-  ( Hom ` D ) = ( Hom ` D )
11 relfunc
 |-  Rel ( C Func D )
12 1st2ndbr
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
13 11 2 12 sylancr
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
14 1 6 10 13 4 5 funcf2
 |-  ( ph -> ( X ( 2nd ` F ) Y ) : ( X H Y ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` D ) ( ( 1st ` F ) ` Y ) ) )
15 fvco3
 |-  ( ( ( X ( 2nd ` F ) Y ) : ( X H Y ) --> ( ( ( 1st ` F ) ` X ) ( Hom ` D ) ( ( 1st ` F ) ` Y ) ) /\ R e. ( X H Y ) ) -> ( ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) )
16 14 7 15 syl2anc
 |-  ( ph -> ( ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) o. ( X ( 2nd ` F ) Y ) ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) )
17 9 16 eqtrd
 |-  ( ph -> ( ( X ( 2nd ` ( G o.func F ) ) Y ) ` R ) = ( ( ( ( 1st ` F ) ` X ) ( 2nd ` G ) ( ( 1st ` F ) ` Y ) ) ` ( ( X ( 2nd ` F ) Y ) ` R ) ) )