Metamath Proof Explorer

Theorem cofu2a

Description: Value of the morphism part of the functor composition. (Contributed by Zhi Wang, 16-Nov-2025)

Ref Expression
Hypotheses cofu1a.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
cofu1a.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
cofu1a.k ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
cofu1a.m ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝑀 , 𝑁 ⟩ )
cofu1a.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
cofu2a.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
cofu2a.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
cofu2a.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion cofu2a ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑋 𝑁 𝑌 ) ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 cofu1a.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 cofu1a.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3 cofu1a.k ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
4 cofu1a.m ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝑀 , 𝑁 ⟩ )
5 cofu1a.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 cofu2a.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 cofu2a.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
8 cofu2a.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
9 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
10 2 9 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
11 df-br ⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
12 3 11 sylib ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
13 1 10 12 5 6 7 8 cofu2 ⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) 𝑌 ) ‘ 𝑅 ) = ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) ‘ 𝑅 ) ) )
14 4 fveq2d ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
15 10 12 cofucl ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ∈ ( 𝐶 Func 𝐸 ) )
16 4 15 eqeltrrd ⊢ ( 𝜑 → ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
17 df-br ⊢ ( 𝑀 ( 𝐶 Func 𝐸 ) 𝑁 ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
18 16 17 sylibr ⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐸 ) 𝑁 )
19 18 func2nd ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑁 )
20 14 19 eqtrd ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = 𝑁 )
21 20 oveqd ⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) 𝑌 ) = ( 𝑋 𝑁 𝑌 ) )
22 21 fveq1d ⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) 𝑌 ) ‘ 𝑅 ) = ( ( 𝑋 𝑁 𝑌 ) ‘ 𝑅 ) )
23 3 func2nd ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
24 2 func1st ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
25 24 fveq1d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
26 24 fveq1d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) )
27 23 25 26 oveq123d ⊢ ( 𝜑 → ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) )
28 2 func2nd ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
29 28 oveqd ⊢ ( 𝜑 → ( 𝑋 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) = ( 𝑋 𝐺 𝑌 ) )
30 29 fveq1d ⊢ ( 𝜑 → ( ( 𝑋 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) ‘ 𝑅 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) )
31 27 30 fveq12d ⊢ ( 𝜑 → ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) ‘ 𝑅 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) )
32 13 22 31 3eqtr3rd ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑋 𝑁 𝑌 ) ‘ 𝑅 ) )