Metamath Proof Explorer


Theorem efmndid

Description: The identity function restricted to a set A is the identity element of the monoid of endofunctions on A . (Contributed by AV, 25-Jan-2024)

Ref Expression
Hypothesis ielefmnd.g No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
Assertion efmndid A V I A = 0 G

Proof

Step Hyp Ref Expression
1 ielefmnd.g Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2 eqid Base G = Base G
3 eqid 0 G = 0 G
4 eqid + G = + G
5 1 ielefmnd A V I A Base G
6 1 2 4 efmndov I A Base G f Base G I A + G f = I A f
7 5 6 sylan A V f Base G I A + G f = I A f
8 1 2 efmndbasf f Base G f : A A
9 8 adantl A V f Base G f : A A
10 fcoi2 f : A A I A f = f
11 9 10 syl A V f Base G I A f = f
12 7 11 eqtrd A V f Base G I A + G f = f
13 5 anim1ci A V f Base G f Base G I A Base G
14 1 2 4 efmndov f Base G I A Base G f + G I A = f I A
15 13 14 syl A V f Base G f + G I A = f I A
16 fcoi1 f : A A f I A = f
17 9 16 syl A V f Base G f I A = f
18 15 17 eqtrd A V f Base G f + G I A = f
19 2 3 4 5 12 18 ismgmid2 A V I A = 0 G