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 No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
Assertion efmndmnd A V G Mnd

Proof

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