Metamath Proof Explorer

Theorem efmndsgrp

Description: The monoid of endofunctions on a class A is a semigroup. (Contributed by AV, 28-Jan-2024)

Ref Expression
Hypothesis efmndmgm.g 
|- G = ( EndoFMnd ` A )
Assertion efmndsgrp 
|- G e. Smgrp

Proof

Step Hyp Ref Expression
1 efmndmgm.g 
 |-  G = ( EndoFMnd ` A )
2 1 efmndmgm 
 |-  G e. Mgm
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 1 3 4 efmndcl 
 |-  ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
6 1 3 4 efmndov 
 |-  ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) = ( x o. y ) )
7 5 6 symggrplem 
 |-  ( ( f e. ( Base ` G ) /\ g e. ( Base ` G ) /\ h e. ( Base ` G ) ) -> ( ( f ( +g ` G ) g ) ( +g ` G ) h ) = ( f ( +g ` G ) ( g ( +g ` G ) h ) ) )
8 7 rgen3 
 |-  A. f e. ( Base ` G ) A. g e. ( Base ` G ) A. h e. ( Base ` G ) ( ( f ( +g ` G ) g ) ( +g ` G ) h ) = ( f ( +g ` G ) ( g ( +g ` G ) h ) )
9 3 4 issgrp 
 |-  ( G e. Smgrp <-> ( G e. Mgm /\ A. f e. ( Base ` G ) A. g e. ( Base ` G ) A. h e. ( Base ` G ) ( ( f ( +g ` G ) g ) ( +g ` G ) h ) = ( f ( +g ` G ) ( g ( +g ` G ) h ) ) ) )
10 2 8 9 mpbir2an 
 |-  G e. Smgrp