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	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		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
4		fvexd	Could not format ( ph -> ( ( End ` C ) ` X ) e. _V ) : No typesetting found for |- ( ph -> ( ( End ` C ) ` X ) e. _V ) with typecode |-
5	3 4	strfvnd	Could not format ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( ( ( End ` C ) ` X ) ` ( +g ` ndx ) ) ) : No typesetting found for |- ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( ( ( End ` C ) ` X ) ` ( +g ` ndx ) ) ) with typecode |-
6	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 |-
7	6	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 |-
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	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 |-