Metamath Proof Explorer

Theorem efmndplusg

Description: The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024)

Ref Expression
Hypotheses efmndtset.g 
|- G = ( EndoFMnd ` A )
efmndplusg.b 
|- B = ( Base ` G )
efmndplusg.p 
|- .+ = ( +g ` G )
Assertion efmndplusg 
|- .+ = ( f e. B , g e. B |-> ( f o. g ) )

Proof

Step Hyp Ref Expression
1 efmndtset.g 
 |-  G = ( EndoFMnd ` A )
2 efmndplusg.b 
 |-  B = ( Base ` G )
3 efmndplusg.p 
 |-  .+ = ( +g ` G )
4 1 2 efmndbas 
 |-  B = ( A ^m A )
5 eqid 
 |-  ( f e. B , g e. B |-> ( f o. g ) ) = ( f e. B , g e. B |-> ( f o. g ) )
6 eqid 
 |-  ( Xt_ ` ( A X. { ~P A } ) ) = ( Xt_ ` ( A X. { ~P A } ) )
7 1 4 5 6 efmnd 
 |-  ( A e. _V -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } )
8 7 fveq2d 
 |-  ( A e. _V -> ( +g ` G ) = ( +g ` { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } ) )
9 2 fvexi 
 |-  B e. _V
10 9 9 mpoex 
 |-  ( f e. B , g e. B |-> ( f o. g ) ) e. _V
11 eqid 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. }
12 11 topgrpplusg 
 |-  ( ( f e. B , g e. B |-> ( f o. g ) ) e. _V -> ( f e. B , g e. B |-> ( f o. g ) ) = ( +g ` { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } ) )
13 10 12 ax-mp 
 |-  ( f e. B , g e. B |-> ( f o. g ) ) = ( +g ` { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( f e. B , g e. B |-> ( f o. g ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( A X. { ~P A } ) ) >. } )
14 8 3 13 3eqtr4g 
 |-  ( A e. _V -> .+ = ( f e. B , g e. B |-> ( f o. g ) ) )
15 fvprc 
 |-  ( -. A e. _V -> ( EndoFMnd ` A ) = (/) )
16 1 15 syl5eq 
 |-  ( -. A e. _V -> G = (/) )
17 16 fveq2d 
 |-  ( -. A e. _V -> ( +g ` G ) = ( +g ` (/) ) )
18 plusgid 
 |-  +g = Slot ( +g ` ndx )
19 18 str0 
 |-  (/) = ( +g ` (/) )
20 17 3 19 3eqtr4g 
 |-  ( -. A e. _V -> .+ = (/) )
21 16 fveq2d 
 |-  ( -. A e. _V -> ( Base ` G ) = ( Base ` (/) ) )
22 base0 
 |-  (/) = ( Base ` (/) )
23 21 2 22 3eqtr4g 
 |-  ( -. A e. _V -> B = (/) )
24 23 olcd 
 |-  ( -. A e. _V -> ( B = (/) \/ B = (/) ) )
25 0mpo0 
 |-  ( ( B = (/) \/ B = (/) ) -> ( f e. B , g e. B |-> ( f o. g ) ) = (/) )
26 24 25 syl 
 |-  ( -. A e. _V -> ( f e. B , g e. B |-> ( f o. g ) ) = (/) )
27 20 26 eqtr4d 
 |-  ( -. A e. _V -> .+ = ( f e. B , g e. B |-> ( f o. g ) ) )
28 14 27 pm2.61i 
 |-  .+ = ( f e. B , g e. B |-> ( f o. g ) )