Metamath Proof Explorer

Theorem bj-endval

Description: Value 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-endval 
|- ( ph -> ( ( End ` C ) ` X ) = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. 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 df-bj-end 
 |-  End = ( c e. Cat |-> ( x e. ( Base ` c ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) )
4 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
5 fveq2 
 |-  ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
6 5 oveqd 
 |-  ( c = C -> ( x ( Hom ` c ) x ) = ( x ( Hom ` C ) x ) )
7 6 opeq2d 
 |-  ( c = C -> <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. = <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. )
8 fveq2 
 |-  ( c = C -> ( comp ` c ) = ( comp ` C ) )
9 8 oveqd 
 |-  ( c = C -> ( <. x , x >. ( comp ` c ) x ) = ( <. x , x >. ( comp ` C ) x ) )
10 9 opeq2d 
 |-  ( c = C -> <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. = <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. )
11 7 10 preq12d 
 |-  ( c = C -> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } = { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } )
12 4 11 mpteq12dv 
 |-  ( c = C -> ( x e. ( Base ` c ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) = ( x e. ( Base ` C ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } ) )
13 fvex 
 |-  ( Base ` C ) e. _V
14 13 mptex 
 |-  ( x e. ( Base ` C ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } ) e. _V
15 14 a1i 
 |-  ( ph -> ( x e. ( Base ` C ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } ) e. _V )
16 3 12 1 15 fvmptd3 
 |-  ( ph -> ( End ` C ) = ( x e. ( Base ` C ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } ) )
17 id 
 |-  ( x = X -> x = X )
18 17 17 oveq12d 
 |-  ( x = X -> ( x ( Hom ` C ) x ) = ( X ( Hom ` C ) X ) )
19 18 opeq2d 
 |-  ( x = X -> <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. = <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. )
20 17 17 opeq12d 
 |-  ( x = X -> <. x , x >. = <. X , X >. )
21 20 17 oveq12d 
 |-  ( x = X -> ( <. x , x >. ( comp ` C ) x ) = ( <. X , X >. ( comp ` C ) X ) )
22 21 opeq2d 
 |-  ( x = X -> <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. = <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. )
23 19 22 preq12d 
 |-  ( x = X -> { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } )
24 23 adantl 
 |-  ( ( ph /\ x = X ) -> { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } )
25 prex 
 |-  { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } e. _V
26 25 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } e. _V )
27 16 24 2 26 fvmptd 
 |-  ( ph -> ( ( End ` C ) ` X ) = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } )