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 \in V \to {I ↾}_{A} = 0_{G}$

Proof

Step	Hyp	Ref	Expression
1		ielefmnd.g	$⊢ G = EndoFMnd (A)$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3		eqid	$⊢ 0_{G} = 0_{G}$
4		eqid	$⊢ +_{G} = +_{G}$
5	1	ielefmnd	$⊢ A \in V \to {I ↾}_{A} \in {Base}_{G}$
6	1 2 4	efmndov	$⊢ ({I ↾}_{A} \in {Base}_{G} \land f \in {Base}_{G}) \to ({I ↾}_{A}) +_{G} f = ({I ↾}_{A}) \circ f$
7	5 6	sylan	$⊢ (A \in V \land f \in {Base}_{G}) \to ({I ↾}_{A}) +_{G} f = ({I ↾}_{A}) \circ f$
8	1 2	efmndbasf	$⊢ f \in {Base}_{G} \to f : A ⟶ A$
9	8	adantl	$⊢ (A \in V \land f \in {Base}_{G}) \to f : A ⟶ A$
10		fcoi2	$⊢ f : A ⟶ A \to ({I ↾}_{A}) \circ f = f$
11	9 10	syl	$⊢ (A \in V \land f \in {Base}_{G}) \to ({I ↾}_{A}) \circ f = f$
12	7 11	eqtrd	$⊢ (A \in V \land f \in {Base}_{G}) \to ({I ↾}_{A}) +_{G} f = f$
13	5	anim1ci	$⊢ (A \in V \land f \in {Base}_{G}) \to (f \in {Base}_{G} \land {I ↾}_{A} \in {Base}_{G})$
14	1 2 4	efmndov	$⊢ (f \in {Base}_{G} \land {I ↾}_{A} \in {Base}_{G}) \to f +_{G} ({I ↾}_{A}) = f \circ ({I ↾}_{A})$
15	13 14	syl	$⊢ (A \in V \land f \in {Base}_{G}) \to f +_{G} ({I ↾}_{A}) = f \circ ({I ↾}_{A})$
16		fcoi1	$⊢ f : A ⟶ A \to f \circ ({I ↾}_{A}) = f$
17	9 16	syl	$⊢ (A \in V \land f \in {Base}_{G}) \to f \circ ({I ↾}_{A}) = f$
18	15 17	eqtrd	$⊢ (A \in V \land f \in {Base}_{G}) \to f +_{G} ({I ↾}_{A}) = f$
19	2 3 4 5 12 18	ismgmid2	$⊢ A \in V \to {I ↾}_{A} = 0_{G}$