Theorem coa2

Description: The morphism part of arrow composition. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homdmcoa.o	$$⊢\underset{\dot{}}{·}={comp}_a\left(C\right)$$
	homdmcoa.h	$$⊢H={Hom}_a\left(C\right)$$
	homdmcoa.f	$$⊢\phi \to F\in \left(XHY\right)$$
	homdmcoa.g	$$⊢\phi \to G\in \left(YHZ\right)$$
	coaval.x	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(C\right)$$
Assertion	coa2	$$⊢\phi \to 2^{nd}\left(G\underset{\dot{}}{·}F\right)=2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		homdmcoa.o	$$⊢\underset{\dot{}}{·}={comp}_a\left(C\right)$$
2		homdmcoa.h	$$⊢H={Hom}_a\left(C\right)$$
3		homdmcoa.f	$$⊢\phi \to F\in \left(XHY\right)$$
4		homdmcoa.g	$$⊢\phi \to G\in \left(YHZ\right)$$
5		coaval.x	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(C\right)$$
6	1 2 3 4 5	coaval	$$⊢\phi \to G\underset{\dot{}}{·}F=⟨X,Z,2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)⟩$$
7	6	fveq2d	$$⊢\phi \to 2^{nd}\left(G\underset{\dot{}}{·}F\right)=2^{nd}\left(⟨X,Z,2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)⟩\right)$$
8		ovex	$$⊢2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)\in \mathrm{V}$$
9		ot3rdg	$$⊢2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)\in \mathrm{V}\to 2^{nd}\left(⟨X,Z,2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)⟩\right)=2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)$$
10	8 9	ax-mp	$$⊢2^{nd}\left(⟨X,Z,2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)⟩\right)=2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)$$
11	7 10	eqtrdi	$$⊢\phi \to 2^{nd}\left(G\underset{\dot{}}{·}F\right)=2^{nd}\left(G\right)\left(⟨X,Y⟩\underset{\dot{}}{\bullet }Z\right)2^{nd}\left(F\right)$$