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 ) ) ) >. )