cofid2

Description: Express the morphism part of ( G o.func F ) = I explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

	Ref	Expression
Hypotheses	cofid1a.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
	cofid1a.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	cofid1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cofid1.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	cofid1.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
	cofid1.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘_func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
	cofid2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	cofid2.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	cofid2.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	cofid2	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		cofid1a.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
2		cofid1a.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		cofid1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		cofid1.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5		cofid1.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
6		cofid1.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘_func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
7		cofid2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		cofid2.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
9		cofid2.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
10	5	func2nd	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
11	4	func1st	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
12	11	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
13	11	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) )
14	10 12 13	oveq123d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) )
15	4	func2nd	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
16	15	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) = ( 𝑋 𝐺 𝑌 ) )
17	16	fveq1d	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) ‘ 𝑅 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) )
18	14 17	fveq12d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) ‘ 𝑅 ) ) = ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) )
19		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
20	4 19	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
21		df-br	⊢ ( 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐸 Func 𝐷 ) )
22	5 21	sylib	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐸 Func 𝐷 ) )
23	1 2 3 20 22 6 7 8 9	cofid2a	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) ‘ ( ( 𝑋 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) ‘ 𝑅 ) ) = 𝑅 )
24	18 23	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = 𝑅 )

Metamath Proof Explorer

Theorem cofid2

Proof