This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )