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	⊢ · = ( compa ‘ 𝐶 )
	homdmcoa.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
	homdmcoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	homdmcoa.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
Assertion	homdmcoa	⊢ ( 𝜑 → 𝐺 dom · 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		homdmcoa.o	⊢ · = ( compa ‘ 𝐶 )
2		homdmcoa.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
3		homdmcoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4		homdmcoa.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
5		eqid	⊢ ( Arrow ‘ 𝐶 ) = ( Arrow ‘ 𝐶 )
6	5 2	homarw	⊢ ( 𝑋 𝐻 𝑌 ) ⊆ ( Arrow ‘ 𝐶 )
7	6 3	sseldi	⊢ ( 𝜑 → 𝐹 ∈ ( Arrow ‘ 𝐶 ) )
8	5 2	homarw	⊢ ( 𝑌 𝐻 𝑍 ) ⊆ ( Arrow ‘ 𝐶 )
9	8 4	sseldi	⊢ ( 𝜑 → 𝐺 ∈ ( Arrow ‘ 𝐶 ) )
10	2	homacd	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( coda ‘ 𝐹 ) = 𝑌 )
11	3 10	syl	⊢ ( 𝜑 → ( coda ‘ 𝐹 ) = 𝑌 )
12	2	homadm	⊢ ( 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) → ( doma ‘ 𝐺 ) = 𝑌 )
13	4 12	syl	⊢ ( 𝜑 → ( doma ‘ 𝐺 ) = 𝑌 )
14	11 13	eqtr4d	⊢ ( 𝜑 → ( coda ‘ 𝐹 ) = ( doma ‘ 𝐺 ) )
15	1 5	eldmcoa	⊢ ( 𝐺 dom · 𝐹 ↔ ( 𝐹 ∈ ( Arrow ‘ 𝐶 ) ∧ 𝐺 ∈ ( Arrow ‘ 𝐶 ) ∧ ( coda ‘ 𝐹 ) = ( doma ‘ 𝐺 ) ) )
16	7 9 14 15	syl3anbrc	⊢ ( 𝜑 → 𝐺 dom · 𝐹 )