Theorem coa2

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

	Ref	Expression
Hypotheses	homdmcoa.o	⊢ · = ( compa ‘ 𝐶 )
	homdmcoa.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
	homdmcoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
	homdmcoa.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
	coaval.x	⊢ ∙ = ( comp ‘ 𝐶 )
Assertion	coa2	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 · 𝐹 ) ) = ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		homdmcoa.o	⊢ · = ( compa ‘ 𝐶 )
2		homdmcoa.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
3		homdmcoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4		homdmcoa.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑍 ) )
5		coaval.x	⊢ ∙ = ( comp ‘ 𝐶 )
6	1 2 3 4 5	coaval	⊢ ( 𝜑 → ( 𝐺 · 𝐹 ) = ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ )
7	6	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 · 𝐹 ) ) = ( 2nd ‘ ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ ) )
8		ovex	⊢ ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ∈ V
9		ot3rdg	⊢ ( ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ∈ V → ( 2nd ‘ ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ ) = ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) )
10	8 9	ax-mp	⊢ ( 2nd ‘ ⟨ 𝑋 , 𝑍 , ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) ⟩ ) = ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) )
11	7 10	eqtrdi	⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 · 𝐹 ) ) = ( ( 2nd ‘ 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ∙ 𝑍 ) ( 2nd ‘ 𝐹 ) ) )