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