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 ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( 𝐺func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( 2nd𝐺 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )

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 ( 𝜑 → ( 𝑋 ( 2nd ‘ ( 𝐺func 𝐹 ) ) 𝑌 ) = ( ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( 2nd𝐺 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ) )
9 8 fveq1d ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( 𝐺func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( 2nd𝐺 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ) ‘ 𝑅 ) )
10 eqid ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
11 relfunc Rel ( 𝐶 Func 𝐷 )
12 1st2ndbr ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
13 11 2 12 sylancr ( 𝜑 → ( 1st𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd𝐹 ) )
14 1 6 10 13 4 5 funcf2 ( 𝜑 → ( 𝑋 ( 2nd𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) )
15 fvco3 ( ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ∧ 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( 2nd𝐺 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ) ‘ 𝑅 ) = ( ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( 2nd𝐺 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )
16 14 7 15 syl2anc ( 𝜑 → ( ( ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( 2nd𝐺 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ) ‘ 𝑅 ) = ( ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( 2nd𝐺 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )
17 9 16 eqtrd ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( 𝐺func 𝐹 ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( 2nd𝐺 ) ( ( 1st𝐹 ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ‘ 𝑅 ) ) )