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	$$⊢\phi \to C\in \mathrm{Cat}$$
	bj-endval.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
Assertion	bj-endcomp	$$⊢\phi \to {+}_{End\left(C\right)\left(X\right)}=⟨X,X⟩\mathrm{comp}\left(C\right)X$$

Proof

Step	Hyp	Ref	Expression
1		bj-endval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		bj-endval.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
3		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
4		fvexd	$$⊢\phi \to End\left(C\right)\left(X\right)\in \mathrm{V}$$
5	3 4	strfvnd	$$⊢\phi \to {+}_{End\left(C\right)\left(X\right)}=End\left(C\right)\left(X\right)\left({+}_{\mathrm{ndx}}\right)$$
6	1 2	bj-endval	$$⊢\phi \to End\left(C\right)\left(X\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}$$
7	6	fveq1d	$$⊢\phi \to End\left(C\right)\left(X\right)\left({+}_{\mathrm{ndx}}\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}\left({+}_{\mathrm{ndx}}\right)$$
8		basendxnplusgndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
9		fvex	$$⊢{+}_{\mathrm{ndx}}\in \mathrm{V}$$
10		ovex	$$⊢⟨X,X⟩\mathrm{comp}\left(C\right)X\in \mathrm{V}$$
11	9 10	fvpr2	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}\left({+}_{\mathrm{ndx}}\right)=⟨X,X⟩\mathrm{comp}\left(C\right)X$$
12	8 11	mp1i	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}\left({+}_{\mathrm{ndx}}\right)=⟨X,X⟩\mathrm{comp}\left(C\right)X$$
13	5 7 12	3eqtrd	$$⊢\phi \to {+}_{End\left(C\right)\left(X\right)}=⟨X,X⟩\mathrm{comp}\left(C\right)X$$