Theorem bj-endcomp

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

	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	Could not format assertion : No typesetting found for |- ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) with typecode |-

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	1 2	bj-endval	Could not format ( ph -> ( ( End ` C ) ` X ) = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) : No typesetting found for |- ( ph -> ( ( End ` C ) ` X ) = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) with typecode |-
4	3	fveq1d	Could not format ( ph -> ( ( ( End ` C ) ` X ) ` ( +g ` ndx ) ) = ( { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ` ( +g ` ndx ) ) ) : No typesetting found for |- ( ph -> ( ( ( End ` C ) ` X ) ` ( +g ` ndx ) ) = ( { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ` ( +g ` ndx ) ) ) with typecode |-
5		fvexd	Could not format ( ph -> ( ( End ` C ) ` X ) e. _V ) : No typesetting found for |- ( ph -> ( ( End ` C ) ` X ) e. _V ) with typecode |-
6		df-plusg	$$⊢{+}_{𝑔}=\mathrm{Slot}2$$
7		2nn	$$⊢2\in \mathbb{N}$$
8	5 6 7	strndxid	Could not format ( ph -> ( ( ( End ` C ) ` X ) ` ( +g ` ndx ) ) = ( +g ` ( ( End ` C ) ` X ) ) ) : No typesetting found for |- ( ph -> ( ( ( End ` C ) ` X ) ` ( +g ` ndx ) ) = ( +g ` ( ( End ` C ) ` X ) ) ) with typecode |-
9		basendxnplusgndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
10		fvex	$$⊢{+}_{\mathrm{ndx}}\in \mathrm{V}$$
11		ovex	$$⊢⟨X,X⟩\mathrm{comp}\left(C\right)X\in \mathrm{V}$$
12	10 11	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$$
13	9 12	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$$
14	4 8 13	3eqtr3d	Could not format ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) : No typesetting found for |- ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) with typecode |-