Theorem bj-endcomp

Description: Composition law of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-endval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	bj-endval.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
Assertion	bj-endcomp	⊢ ( 𝜑 → ( +g ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-endval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		bj-endval.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
3		plusgid	⊢ +g = Slot ( +g ‘ ndx )
4		fvexd	⊢ ( 𝜑 → ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ∈ V )
5	3 4	strfvnd	⊢ ( 𝜑 → ( +g ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ‘ ( +g ‘ ndx ) ) )
6	1 2	bj-endval	⊢ ( 𝜑 → ( ( End ‘ 𝐶 ) ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } )
7	6	fveq1d	⊢ ( 𝜑 → ( ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ‘ ( +g ‘ ndx ) ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } ‘ ( +g ‘ ndx ) ) )
8		basendxnplusgndx	⊢ ( Base ‘ ndx ) ≠ ( +g ‘ ndx )
9		fvex	⊢ ( +g ‘ ndx ) ∈ V
10		ovex	⊢ ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ∈ V
11	9 10	fvpr2	⊢ ( ( Base ‘ ndx ) ≠ ( +g ‘ ndx ) → ( { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } ‘ ( +g ‘ ndx ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )
12	8 11	mp1i	⊢ ( 𝜑 → ( { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } ‘ ( +g ‘ ndx ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )
13	5 7 12	3eqtrd	⊢ ( 𝜑 → ( +g ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )