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