Theorem coahom

Description: The composition of two composable arrows is an arrow. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homdmcoa.o	|- .x. = ( compA ` C )
	homdmcoa.h	|- H = ( HomA ` C )
	homdmcoa.f	|- ( ph -> F e. ( X H Y ) )
	homdmcoa.g	|- ( ph -> G e. ( Y H Z ) )
Assertion	coahom	|- ( ph -> ( G .x. F ) e. ( X H Z ) )

Proof

Step	Hyp	Ref	Expression
1		homdmcoa.o	|- .x. = ( compA ` C )
2		homdmcoa.h	|- H = ( HomA ` C )
3		homdmcoa.f	|- ( ph -> F e. ( X H Y ) )
4		homdmcoa.g	|- ( ph -> G e. ( Y H Z ) )
5		eqid	|- ( comp ` C ) = ( comp ` C )
6	1 2 3 4 5	coaval	|- ( ph -> ( G .x. F ) = <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. ( comp ` C ) Z ) ( 2nd ` F ) ) >. )
7		eqid	|- ( Base ` C ) = ( Base ` C )
8	2	homarcl	|- ( F e. ( X H Y ) -> C e. Cat )
9	3 8	syl	|- ( ph -> C e. Cat )
10		eqid	|- ( Hom ` C ) = ( Hom ` C )
11	2 7	homarcl2	|- ( F e. ( X H Y ) -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
12	3 11	syl	|- ( ph -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
13	12	simpld	|- ( ph -> X e. ( Base ` C ) )
14	2 7	homarcl2	|- ( G e. ( Y H Z ) -> ( Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) )
15	4 14	syl	|- ( ph -> ( Y e. ( Base ` C ) /\ Z e. ( Base ` C ) ) )
16	15	simprd	|- ( ph -> Z e. ( Base ` C ) )
17	12	simprd	|- ( ph -> Y e. ( Base ` C ) )
18	2 10	homahom	|- ( F e. ( X H Y ) -> ( 2nd ` F ) e. ( X ( Hom ` C ) Y ) )
19	3 18	syl	|- ( ph -> ( 2nd ` F ) e. ( X ( Hom ` C ) Y ) )
20	2 10	homahom	|- ( G e. ( Y H Z ) -> ( 2nd ` G ) e. ( Y ( Hom ` C ) Z ) )
21	4 20	syl	|- ( ph -> ( 2nd ` G ) e. ( Y ( Hom ` C ) Z ) )
22	7 10 5 9 13 17 16 19 21	catcocl	|- ( ph -> ( ( 2nd ` G ) ( <. X , Y >. ( comp ` C ) Z ) ( 2nd ` F ) ) e. ( X ( Hom ` C ) Z ) )
23	2 7 9 10 13 16 22	elhomai2	|- ( ph -> <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. ( comp ` C ) Z ) ( 2nd ` F ) ) >. e. ( X H Z ) )
24	6 23	eqeltrd	|- ( ph -> ( G .x. F ) e. ( X H Z ) )