Metamath Proof Explorer

Theorem efmndmnd

Description: The monoid of endofunctions on a set A is actually a monoid. (Contributed by AV, 31-Jan-2024)

Ref Expression
Hypothesis ielefmnd.g 
|- G = ( EndoFMnd ` A )
Assertion efmndmnd 
|- ( A e. V -> G e. Mnd )

Proof

Step Hyp Ref Expression
1 ielefmnd.g 
 |-  G = ( EndoFMnd ` A )
2 1 efmndsgrp 
 |-  G e. Smgrp
3 2 a1i 
 |-  ( A e. V -> G e. Smgrp )
4 1 ielefmnd 
 |-  ( A e. V -> ( _I |` A ) e. ( Base ` G ) )
5 oveq1 
 |-  ( i = ( _I |` A ) -> ( i ( +g ` G ) f ) = ( ( _I |` A ) ( +g ` G ) f ) )
6 5 eqeq1d 
 |-  ( i = ( _I |` A ) -> ( ( i ( +g ` G ) f ) = f <-> ( ( _I |` A ) ( +g ` G ) f ) = f ) )
7 oveq2 
 |-  ( i = ( _I |` A ) -> ( f ( +g ` G ) i ) = ( f ( +g ` G ) ( _I |` A ) ) )
8 7 eqeq1d 
 |-  ( i = ( _I |` A ) -> ( ( f ( +g ` G ) i ) = f <-> ( f ( +g ` G ) ( _I |` A ) ) = f ) )
9 6 8 anbi12d 
 |-  ( i = ( _I |` A ) -> ( ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) <-> ( ( ( _I |` A ) ( +g ` G ) f ) = f /\ ( f ( +g ` G ) ( _I |` A ) ) = f ) ) )
10 9 ralbidv 
 |-  ( i = ( _I |` A ) -> ( A. f e. ( Base ` G ) ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) <-> A. f e. ( Base ` G ) ( ( ( _I |` A ) ( +g ` G ) f ) = f /\ ( f ( +g ` G ) ( _I |` A ) ) = f ) ) )
11 10 adantl 
 |-  ( ( A e. V /\ i = ( _I |` A ) ) -> ( A. f e. ( Base ` G ) ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) <-> A. f e. ( Base ` G ) ( ( ( _I |` A ) ( +g ` G ) f ) = f /\ ( f ( +g ` G ) ( _I |` A ) ) = f ) ) )
12 eqid 
 |-  ( Base ` G ) = ( Base ` G )
13 1 12 efmndbasf 
 |-  ( f e. ( Base ` G ) -> f : A --> A )
14 13 adantl 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> f : A --> A )
15 fcoi2 
 |-  ( f : A --> A -> ( ( _I |` A ) o. f ) = f )
16 fcoi1 
 |-  ( f : A --> A -> ( f o. ( _I |` A ) ) = f )
17 15 16 jca 
 |-  ( f : A --> A -> ( ( ( _I |` A ) o. f ) = f /\ ( f o. ( _I |` A ) ) = f ) )
18 14 17 syl 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( ( _I |` A ) o. f ) = f /\ ( f o. ( _I |` A ) ) = f ) )
19 eqid 
 |-  ( +g ` G ) = ( +g ` G )
20 1 12 19 efmndov 
 |-  ( ( ( _I |` A ) e. ( Base ` G ) /\ f e. ( Base ` G ) ) -> ( ( _I |` A ) ( +g ` G ) f ) = ( ( _I |` A ) o. f ) )
21 4 20 sylan 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( _I |` A ) ( +g ` G ) f ) = ( ( _I |` A ) o. f ) )
22 21 eqeq1d 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( ( _I |` A ) ( +g ` G ) f ) = f <-> ( ( _I |` A ) o. f ) = f ) )
23 4 anim1ci 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( f e. ( Base ` G ) /\ ( _I |` A ) e. ( Base ` G ) ) )
24 1 12 19 efmndov 
 |-  ( ( f e. ( Base ` G ) /\ ( _I |` A ) e. ( Base ` G ) ) -> ( f ( +g ` G ) ( _I |` A ) ) = ( f o. ( _I |` A ) ) )
25 23 24 syl 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( f ( +g ` G ) ( _I |` A ) ) = ( f o. ( _I |` A ) ) )
26 25 eqeq1d 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( f ( +g ` G ) ( _I |` A ) ) = f <-> ( f o. ( _I |` A ) ) = f ) )
27 22 26 anbi12d 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( ( ( _I |` A ) ( +g ` G ) f ) = f /\ ( f ( +g ` G ) ( _I |` A ) ) = f ) <-> ( ( ( _I |` A ) o. f ) = f /\ ( f o. ( _I |` A ) ) = f ) ) )
28 18 27 mpbird 
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( ( _I |` A ) ( +g ` G ) f ) = f /\ ( f ( +g ` G ) ( _I |` A ) ) = f ) )
29 28 ralrimiva 
 |-  ( A e. V -> A. f e. ( Base ` G ) ( ( ( _I |` A ) ( +g ` G ) f ) = f /\ ( f ( +g ` G ) ( _I |` A ) ) = f ) )
30 4 11 29 rspcedvd 
 |-  ( A e. V -> E. i e. ( Base ` G ) A. f e. ( Base ` G ) ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) )
31 12 19 ismnddef 
 |-  ( G e. Mnd <-> ( G e. Smgrp /\ E. i e. ( Base ` G ) A. f e. ( Base ` G ) ( ( i ( +g ` G ) f ) = f /\ ( f ( +g ` G ) i ) = f ) ) )
32 3 30 31 sylanbrc 
 |-  ( A e. V -> G e. Mnd )