Metamath Proof Explorer

Theorem cofuass

Description: Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses cofuass.g 
|- ( ph -> G e. ( C Func D ) )
cofuass.h 
|- ( ph -> H e. ( D Func E ) )
cofuass.k 
|- ( ph -> K e. ( E Func F ) )
Assertion cofuass 
|- ( ph -> ( ( K o.func H ) o.func G ) = ( K o.func ( H o.func G ) ) )

Proof

Step Hyp Ref Expression
1 cofuass.g 
 |-  ( ph -> G e. ( C Func D ) )
2 cofuass.h 
 |-  ( ph -> H e. ( D Func E ) )
3 cofuass.k 
 |-  ( ph -> K e. ( E Func F ) )
4 coass 
 |-  ( ( ( 1st ` K ) o. ( 1st ` H ) ) o. ( 1st ` G ) ) = ( ( 1st ` K ) o. ( ( 1st ` H ) o. ( 1st ` G ) ) )
5 eqid 
 |-  ( Base ` D ) = ( Base ` D )
6 5 2 3 cofu1st 
 |-  ( ph -> ( 1st ` ( K o.func H ) ) = ( ( 1st ` K ) o. ( 1st ` H ) ) )
7 6 coeq1d 
 |-  ( ph -> ( ( 1st ` ( K o.func H ) ) o. ( 1st ` G ) ) = ( ( ( 1st ` K ) o. ( 1st ` H ) ) o. ( 1st ` G ) ) )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 8 1 2 cofu1st 
 |-  ( ph -> ( 1st ` ( H o.func G ) ) = ( ( 1st ` H ) o. ( 1st ` G ) ) )
10 9 coeq2d 
 |-  ( ph -> ( ( 1st ` K ) o. ( 1st ` ( H o.func G ) ) ) = ( ( 1st ` K ) o. ( ( 1st ` H ) o. ( 1st ` G ) ) ) )
11 4 7 10 3eqtr4a 
 |-  ( ph -> ( ( 1st ` ( K o.func H ) ) o. ( 1st ` G ) ) = ( ( 1st ` K ) o. ( 1st ` ( H o.func G ) ) ) )
12 coass 
 |-  ( ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) ) o. ( x ( 2nd ` G ) y ) ) = ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) )
13 2 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> H e. ( D Func E ) )
14 3 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> K e. ( E Func F ) )
15 relfunc 
 |-  Rel ( C Func D )
16 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
17 15 1 16 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
18 17 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
19 8 5 18 funcf1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` D ) )
20 simp2 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> x e. ( Base ` C ) )
21 19 20 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
22 simp3 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> y e. ( Base ` C ) )
23 19 22 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` G ) ` y ) e. ( Base ` D ) )
24 5 13 14 21 23 cofu2nd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) = ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) ) )
25 24 coeq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) = ( ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) ) o. ( x ( 2nd ` G ) y ) ) )
26 1 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> G e. ( C Func D ) )
27 8 26 13 20 cofu1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` ( H o.func G ) ) ` x ) = ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) )
28 8 26 13 22 cofu1 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( 1st ` ( H o.func G ) ) ` y ) = ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) )
29 27 28 oveq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) = ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) )
30 8 26 13 20 22 cofu2nd 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( 2nd ` ( H o.func G ) ) y ) = ( ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) )
31 29 30 coeq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) = ( ( ( ( 1st ` H ) ` ( ( 1st ` G ) ` x ) ) ( 2nd ` K ) ( ( 1st ` H ) ` ( ( 1st ` G ) ` y ) ) ) o. ( ( ( ( 1st ` G ) ` x ) ( 2nd ` H ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) )
32 12 25 31 3eqtr4a 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) = ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) )
33 32 mpoeq3dva 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) ) )
34 11 33 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( K o.func H ) ) o. ( 1st ` G ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) >. = <. ( ( 1st ` K ) o. ( 1st ` ( H o.func G ) ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) ) >. )
35 2 3 cofucl 
 |-  ( ph -> ( K o.func H ) e. ( D Func F ) )
36 8 1 35 cofuval 
 |-  ( ph -> ( ( K o.func H ) o.func G ) = <. ( ( 1st ` ( K o.func H ) ) o. ( 1st ` G ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` G ) ` x ) ( 2nd ` ( K o.func H ) ) ( ( 1st ` G ) ` y ) ) o. ( x ( 2nd ` G ) y ) ) ) >. )
37 1 2 cofucl 
 |-  ( ph -> ( H o.func G ) e. ( C Func E ) )
38 8 37 3 cofuval 
 |-  ( ph -> ( K o.func ( H o.func G ) ) = <. ( ( 1st ` K ) o. ( 1st ` ( H o.func G ) ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` ( H o.func G ) ) ` x ) ( 2nd ` K ) ( ( 1st ` ( H o.func G ) ) ` y ) ) o. ( x ( 2nd ` ( H o.func G ) ) y ) ) ) >. )
39 34 36 38 3eqtr4d 
 |-  ( ph -> ( ( K o.func H ) o.func G ) = ( K o.func ( H o.func G ) ) )