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

Metamath Proof Explorer

Theorem efmndsgrp

Description: The monoid of endofunctions on a class A is a semigroup. (Contributed by AV, 28-Jan-2024)

Ref Expression
Hypothesis efmndmgm.g ⊢ G = EndoFMnd ⁡ A
Assertion efmndsgrp ⊢ G ∈ Smgrp

Proof

Step Hyp Ref Expression
1 efmndmgm.g ⊢ G = EndoFMnd ⁡ A
2 1 efmndmgm ⊢ G ∈ Mgm
3 eqid ⊢ Base G = Base G
4 eqid ⊢ + G = + G
5 1 3 4 efmndcl ⊢ x ∈ Base G ∧ y ∈ Base G → x + G y ∈ Base G
6 1 3 4 efmndov ⊢ x ∈ Base G ∧ y ∈ Base G → x + G y = x ∘ y
7 5 6 symggrplem ⊢ f ∈ Base G ∧ g ∈ Base G ∧ h ∈ Base G → f + G g + G h = f + G g + G h
8 7 rgen3 ⊢ ∀ f ∈ Base G ∀ g ∈ Base G ∀ h ∈ Base G f + G g + G h = f + G g + G h
9 3 4 issgrp ⊢ G ∈ Smgrp ↔ G ∈ Mgm ∧ ∀ f ∈ Base G ∀ g ∈ Base G ∀ h ∈ Base G f + G g + G h = f + G g + G h
10 2 8 9 mpbir2an ⊢ G ∈ Smgrp