Theorem homdmcoa

Description: If F : X --> Y and G : Y --> Z , then G and F are composable. (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)$$
Assertion	homdmcoa	$$⊢\phi \to G\mathrm{dom}\underset{\dot{}}{·}F$$

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		eqid	$$⊢\mathrm{Arrow}\left(C\right)=\mathrm{Arrow}\left(C\right)$$
6	5 2	homarw	$$⊢XHY\subseteq \mathrm{Arrow}\left(C\right)$$
7	6 3	sselid	$$⊢\phi \to F\in \mathrm{Arrow}\left(C\right)$$
8	5 2	homarw	$$⊢YHZ\subseteq \mathrm{Arrow}\left(C\right)$$
9	8 4	sselid	$$⊢\phi \to G\in \mathrm{Arrow}\left(C\right)$$
10	2	homacd	$$⊢F\in \left(XHY\right)\to {cod}_a\left(F\right)=Y$$
11	3 10	syl	$$⊢\phi \to {cod}_a\left(F\right)=Y$$
12	2	homadm	$$⊢G\in \left(YHZ\right)\to {dom}_a\left(G\right)=Y$$
13	4 12	syl	$$⊢\phi \to {dom}_a\left(G\right)=Y$$
14	11 13	eqtr4d	$$⊢\phi \to {cod}_a\left(F\right)={dom}_a\left(G\right)$$
15	1 5	eldmcoa	$$⊢G\mathrm{dom}\underset{\dot{}}{·}F\leftrightarrow \left(F\in \mathrm{Arrow}\left(C\right)\wedge G\in \mathrm{Arrow}\left(C\right)\wedge {cod}_a\left(F\right)={dom}_a\left(G\right)\right)$$
16	7 9 14 15	syl3anbrc	$$⊢\phi \to G\mathrm{dom}\underset{\dot{}}{·}F$$