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
|- G = ( EndoFMnd ` A )
Assertion efmndid
|- ( A e. V -> ( _I |` A ) = ( 0g ` G ) )

Proof

Step Hyp Ref Expression
1 ielefmnd.g
 |-  G = ( EndoFMnd ` A )
2 eqid
 |-  ( Base ` G ) = ( Base ` G )
3 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
4 eqid
 |-  ( +g ` G ) = ( +g ` G )
5 1 ielefmnd
 |-  ( A e. V -> ( _I |` A ) e. ( Base ` G ) )
6 1 2 4 efmndov
 |-  ( ( ( _I |` A ) e. ( Base ` G ) /\ f e. ( Base ` G ) ) -> ( ( _I |` A ) ( +g ` G ) f ) = ( ( _I |` A ) o. f ) )
7 5 6 sylan
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( _I |` A ) ( +g ` G ) f ) = ( ( _I |` A ) o. f ) )
8 1 2 efmndbasf
 |-  ( f e. ( Base ` G ) -> f : A --> A )
9 8 adantl
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> f : A --> A )
10 fcoi2
 |-  ( f : A --> A -> ( ( _I |` A ) o. f ) = f )
11 9 10 syl
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( _I |` A ) o. f ) = f )
12 7 11 eqtrd
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( ( _I |` A ) ( +g ` G ) f ) = f )
13 5 anim1ci
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( f e. ( Base ` G ) /\ ( _I |` A ) e. ( Base ` G ) ) )
14 1 2 4 efmndov
 |-  ( ( f e. ( Base ` G ) /\ ( _I |` A ) e. ( Base ` G ) ) -> ( f ( +g ` G ) ( _I |` A ) ) = ( f o. ( _I |` A ) ) )
15 13 14 syl
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( f ( +g ` G ) ( _I |` A ) ) = ( f o. ( _I |` A ) ) )
16 fcoi1
 |-  ( f : A --> A -> ( f o. ( _I |` A ) ) = f )
17 9 16 syl
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( f o. ( _I |` A ) ) = f )
18 15 17 eqtrd
 |-  ( ( A e. V /\ f e. ( Base ` G ) ) -> ( f ( +g ` G ) ( _I |` A ) ) = f )
19 2 3 4 5 12 18 ismgmid2
 |-  ( A e. V -> ( _I |` A ) = ( 0g ` G ) )