Metamath Proof Explorer

Theorem cofuval2

Description: Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses cofuval2.b 
|- B = ( Base ` C )
cofuval2.f 
|- ( ph -> F ( C Func D ) G )
cofuval2.x 
|- ( ph -> H ( D Func E ) K )
Assertion cofuval2 
|- ( ph -> ( <. H , K >. o.func <. F , G >. ) = <. ( H o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) K ( F ` y ) ) o. ( x G y ) ) ) >. )

Proof

Step Hyp Ref Expression
1 cofuval2.b 
 |-  B = ( Base ` C )
2 cofuval2.f 
 |-  ( ph -> F ( C Func D ) G )
3 cofuval2.x 
 |-  ( ph -> H ( D Func E ) K )
4 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
5 2 4 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
6 df-br 
 |-  ( H ( D Func E ) K <-> <. H , K >. e. ( D Func E ) )
7 3 6 sylib 
 |-  ( ph -> <. H , K >. e. ( D Func E ) )
8 1 5 7 cofuval 
 |-  ( ph -> ( <. H , K >. o.func <. F , G >. ) = <. ( ( 1st ` <. H , K >. ) o. ( 1st ` <. F , G >. ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` <. F , G >. ) ` x ) ( 2nd ` <. H , K >. ) ( ( 1st ` <. F , G >. ) ` y ) ) o. ( x ( 2nd ` <. F , G >. ) y ) ) ) >. )
9 relfunc 
 |-  Rel ( D Func E )
10 brrelex12 
 |-  ( ( Rel ( D Func E ) /\ H ( D Func E ) K ) -> ( H e. _V /\ K e. _V ) )
11 9 3 10 sylancr 
 |-  ( ph -> ( H e. _V /\ K e. _V ) )
12 op1stg 
 |-  ( ( H e. _V /\ K e. _V ) -> ( 1st ` <. H , K >. ) = H )
13 11 12 syl 
 |-  ( ph -> ( 1st ` <. H , K >. ) = H )
14 relfunc 
 |-  Rel ( C Func D )
15 brrelex12 
 |-  ( ( Rel ( C Func D ) /\ F ( C Func D ) G ) -> ( F e. _V /\ G e. _V ) )
16 14 2 15 sylancr 
 |-  ( ph -> ( F e. _V /\ G e. _V ) )
17 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
18 16 17 syl 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
19 13 18 coeq12d 
 |-  ( ph -> ( ( 1st ` <. H , K >. ) o. ( 1st ` <. F , G >. ) ) = ( H o. F ) )
20 op2ndg 
 |-  ( ( H e. _V /\ K e. _V ) -> ( 2nd ` <. H , K >. ) = K )
21 11 20 syl 
 |-  ( ph -> ( 2nd ` <. H , K >. ) = K )
22 21 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( 2nd ` <. H , K >. ) = K )
23 18 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( 1st ` <. F , G >. ) = F )
24 23 fveq1d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( 1st ` <. F , G >. ) ` x ) = ( F ` x ) )
25 23 fveq1d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( 1st ` <. F , G >. ) ` y ) = ( F ` y ) )
26 22 24 25 oveq123d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( ( 1st ` <. F , G >. ) ` x ) ( 2nd ` <. H , K >. ) ( ( 1st ` <. F , G >. ) ` y ) ) = ( ( F ` x ) K ( F ` y ) ) )
27 op2ndg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 2nd ` <. F , G >. ) = G )
28 16 27 syl 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
29 28 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( 2nd ` <. F , G >. ) = G )
30 29 oveqd 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x ( 2nd ` <. F , G >. ) y ) = ( x G y ) )
31 26 30 coeq12d 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( ( ( ( 1st ` <. F , G >. ) ` x ) ( 2nd ` <. H , K >. ) ( ( 1st ` <. F , G >. ) ` y ) ) o. ( x ( 2nd ` <. F , G >. ) y ) ) = ( ( ( F ` x ) K ( F ` y ) ) o. ( x G y ) ) )
32 31 mpoeq3dva 
 |-  ( ph -> ( x e. B , y e. B |-> ( ( ( ( 1st ` <. F , G >. ) ` x ) ( 2nd ` <. H , K >. ) ( ( 1st ` <. F , G >. ) ` y ) ) o. ( x ( 2nd ` <. F , G >. ) y ) ) ) = ( x e. B , y e. B |-> ( ( ( F ` x ) K ( F ` y ) ) o. ( x G y ) ) ) )
33 19 32 opeq12d 
 |-  ( ph -> <. ( ( 1st ` <. H , K >. ) o. ( 1st ` <. F , G >. ) ) , ( x e. B , y e. B |-> ( ( ( ( 1st ` <. F , G >. ) ` x ) ( 2nd ` <. H , K >. ) ( ( 1st ` <. F , G >. ) ` y ) ) o. ( x ( 2nd ` <. F , G >. ) y ) ) ) >. = <. ( H o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) K ( F ` y ) ) o. ( x G y ) ) ) >. )
34 8 33 eqtrd 
 |-  ( ph -> ( <. H , K >. o.func <. F , G >. ) = <. ( H o. F ) , ( x e. B , y e. B |-> ( ( ( F ` x ) K ( F ` y ) ) o. ( x G y ) ) ) >. )