Metamath Proof Explorer

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 
|- ( ph -> C e. Cat )
bj-endval.x 
|- ( ph -> X e. ( Base ` C ) )
Assertion bj-endcomp 
|- ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) )

Proof

Step Hyp Ref Expression
1 bj-endval.c 
 |-  ( ph -> C e. Cat )
2 bj-endval.x 
 |-  ( ph -> X e. ( Base ` C ) )
3 plusgid 
 |-  +g = Slot ( +g ` ndx )
4 fvexd 
 |-  ( ph -> ( ( End ` C ) ` X ) e. _V )
5 3 4 strfvnd 
 |-  ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( ( ( End ` C ) ` X ) ` ( +g ` ndx ) ) )
6 1 2 bj-endval 
 |-  ( ph -> ( ( End ` C ) ` X ) = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } )
7 6 fveq1d 
 |-  ( ph -> ( ( ( End ` C ) ` X ) ` ( +g ` ndx ) ) = ( { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ` ( +g ` ndx ) ) )
8 basendxnplusgndx 
 |-  ( Base ` ndx ) =/= ( +g ` ndx )
9 fvex 
 |-  ( +g ` ndx ) e. _V
10 ovex 
 |-  ( <. X , X >. ( comp ` C ) X ) e. _V
11 9 10 fvpr2 
 |-  ( ( Base ` ndx ) =/= ( +g ` ndx ) -> ( { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ` ( +g ` ndx ) ) = ( <. X , X >. ( comp ` C ) X ) )
12 8 11 mp1i 
 |-  ( ph -> ( { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ` ( +g ` ndx ) ) = ( <. X , X >. ( comp ` C ) X ) )
13 5 7 12 3eqtrd 
 |-  ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) )