Theorem coa2

Description: The morphism part of arrow composition. (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 ) )
	coaval.x	|- .xb = ( comp ` C )
Assertion	coa2	|- ( ph -> ( 2nd ` ( G .x. F ) ) = ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) )

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		coaval.x	|- .xb = ( comp ` C )
6	1 2 3 4 5	coaval	|- ( ph -> ( G .x. F ) = <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. )
7	6	fveq2d	|- ( ph -> ( 2nd ` ( G .x. F ) ) = ( 2nd ` <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. ) )
8		ovex	|- ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) e. _V
9		ot3rdg	|- ( ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) e. _V -> ( 2nd ` <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. ) = ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) )
10	8 9	ax-mp	|- ( 2nd ` <. X , Z , ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) >. ) = ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) )
11	7 10	eqtrdi	|- ( ph -> ( 2nd ` ( G .x. F ) ) = ( ( 2nd ` G ) ( <. X , Y >. .xb Z ) ( 2nd ` F ) ) )