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