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 eqtrid
 |-  ( -. 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 ) )