Metamath Proof Explorer


Theorem cofuval

Description: Value of the composition of two functors. (Contributed by Mario Carneiro, 3-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 ) )
Assertion cofuval
|- ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )

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 df-cofu
 |-  o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
5 4 a1i
 |-  ( ph -> o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. ) )
6 simprl
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> g = G )
7 6 fveq2d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( 1st ` g ) = ( 1st ` G ) )
8 simprr
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> f = F )
9 8 fveq2d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( 1st ` f ) = ( 1st ` F ) )
10 7 9 coeq12d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( 1st ` g ) o. ( 1st ` f ) ) = ( ( 1st ` G ) o. ( 1st ` F ) ) )
11 8 fveq2d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( 2nd ` f ) = ( 2nd ` F ) )
12 11 dmeqd
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> dom ( 2nd ` f ) = dom ( 2nd ` F ) )
13 relfunc
 |-  Rel ( C Func D )
14 1st2ndbr
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
15 13 2 14 sylancr
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
16 1 15 funcfn2
 |-  ( ph -> ( 2nd ` F ) Fn ( B X. B ) )
17 16 fndmd
 |-  ( ph -> dom ( 2nd ` F ) = ( B X. B ) )
18 17 adantr
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> dom ( 2nd ` F ) = ( B X. B ) )
19 12 18 eqtrd
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> dom ( 2nd ` f ) = ( B X. B ) )
20 19 dmeqd
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> dom dom ( 2nd ` f ) = dom ( B X. B ) )
21 dmxpid
 |-  dom ( B X. B ) = B
22 20 21 eqtrdi
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> dom dom ( 2nd ` f ) = B )
23 6 fveq2d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( 2nd ` g ) = ( 2nd ` G ) )
24 9 fveq1d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` F ) ` x ) )
25 9 fveq1d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( 1st ` f ) ` y ) = ( ( 1st ` F ) ` y ) )
26 23 24 25 oveq123d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) = ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) )
27 11 oveqd
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( x ( 2nd ` f ) y ) = ( x ( 2nd ` F ) y ) )
28 26 27 coeq12d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) )
29 22 22 28 mpoeq123dv
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) = ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) )
30 10 29 opeq12d
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )
31 3 elexd
 |-  ( ph -> G e. _V )
32 2 elexd
 |-  ( ph -> F e. _V )
33 opex
 |-  <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. e. _V
34 33 a1i
 |-  ( ph -> <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. e. _V )
35 5 30 31 32 34 ovmpod
 |-  ( ph -> ( G o.func F ) = <. ( ( 1st ` G ) o. ( 1st ` F ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` G ) ( ( 1st ` F ) ` y ) ) o. ( x ( 2nd ` F ) y ) ) ) >. )