Theorem coahom

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

	Ref	Expression
Hypotheses	homdmcoa.o	⊢ · = ( compa ‘ 𝐶 )
	homdmcoa.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
	homdmcoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	homdmcoa.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
Assertion	coahom	⊢ ( 𝜑 → ( 𝐺 · 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		homdmcoa.o	⊢ · = ( compa ‘ 𝐶 )
2		homdmcoa.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
3		homdmcoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4		homdmcoa.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
5		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
6	1 2 3 4 5	coaval	⊢ ( 𝜑 → ( 𝐺 · 𝐹 ) = ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ )
7		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8	2	homarcl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )
9	3 8	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
10		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
11	2 7	homarcl2	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
12	3 11	syl	⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
13	12	simpld	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
14	2 7	homarcl2	⊢ ( 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) → ( 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) )
15	4 14	syl	⊢ ( 𝜑 → ( 𝑌 ∈ ( Base ‘ 𝐶 ) ∧ 𝑍 ∈ ( Base ‘ 𝐶 ) ) )
16	15	simprd	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
17	12	simprd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
18	2 10	homahom	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 2nd ‘ 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
19	3 18	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
20	2 10	homahom	⊢ ( 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) → ( 2nd ‘ 𝐺 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
21	4 20	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝐺 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑍 ) )
22	7 10 5 9 13 17 16 19 21	catcocl	⊢ ( 𝜑 → ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 2nd ‘ 𝐹 ) ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) )
23	2 7 9 10 13 16 22	elhomai2	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ ∈ ( 𝑋 𝐻 𝑍 ) )
24	6 23	eqeltrd	⊢ ( 𝜑 → ( 𝐺 · 𝐹 ) ∈ ( 𝑋 𝐻 𝑍 ) )