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 ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
Assertion efmndsgrp 𝐺 ∈ Smgrp

Proof

Step Hyp Ref Expression
1 efmndmgm.g ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 1 efmndmgm ⊢ 𝐺 ∈ Mgm
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 1 3 4 efmndcl ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
6 1 3 4 efmndov ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
7 5 6 symggrplem ⊢ ( ( 𝑓 ∈ ( Base ‘ 𝐺 ) ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ∧ ℎ ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) ( +g ‘ 𝐺 ) ℎ ) = ( 𝑓 ( +g ‘ 𝐺 ) ( 𝑔 ( +g ‘ 𝐺 ) ℎ ) ) )
8 7 rgen3 ⊢ ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ∀ 𝑔 ∈ ( Base ‘ 𝐺 ) ∀ ℎ ∈ ( Base ‘ 𝐺 ) ( ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) ( +g ‘ 𝐺 ) ℎ ) = ( 𝑓 ( +g ‘ 𝐺 ) ( 𝑔 ( +g ‘ 𝐺 ) ℎ ) )
9 3 4 issgrp ⊢ ( 𝐺 ∈ Smgrp ↔ ( 𝐺 ∈ Mgm ∧ ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ∀ 𝑔 ∈ ( Base ‘ 𝐺 ) ∀ ℎ ∈ ( Base ‘ 𝐺 ) ( ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) ( +g ‘ 𝐺 ) ℎ ) = ( 𝑓 ( +g ‘ 𝐺 ) ( 𝑔 ( +g ‘ 𝐺 ) ℎ ) ) ) )
10 2 8 9 mpbir2an ⊢ 𝐺 ∈ Smgrp