Metamath Proof Explorer

Theorem cofu2

Description: Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 28-Jan-2017)

		Ref	Expression
	Hypotheses	cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
		cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
		cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
		cofu2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
		cofu2nd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
		cofu2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
		cofu2.y	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
	Assertion	cofu2	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
4		cofu2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		cofu2nd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		cofu2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
7		cofu2.y	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
8	1 2 3 4 5	cofu2nd	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑌 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) )
9	8	fveq1d	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) ‘ 𝑅 ) )
10		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
11		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
12		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
13	11 2 12	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
14	1 6 10 13 4 5	funcf2	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
15		fvco3	⊢ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) ‘ 𝑅 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )
16	14 7 15	syl2anc	⊢ ( 𝜑 → ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) ‘ 𝑅 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )
17	9 16	eqtrd	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )