Theorem sgrpidmnd

Description: A semigroup with an identity element which is not the empty set is a monoid. Of course there could be monoids with the empty set as identity element (see, for example, the monoid of the power set of a class under union, pwmnd and pwmndid ), but these cannot be proven to be monoids with this theorem. (Contributed by AV, 29-Jan-2024)

	Ref	Expression
Hypotheses	sgrpidmnd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	sgrpidmnd.0	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	sgrpidmnd	⊢ ( ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ( 𝑒 ≠ ∅ ∧ 𝑒 = 0 ) ) → 𝐺 ∈ Mnd )

Proof

Step	Hyp	Ref	Expression
1		sgrpidmnd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		sgrpidmnd.0	⊢ 0 = ( 0g ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4	1 3 2	grpidval	⊢ 0 = ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 ) ) )
5	4	eqeq2i	⊢ ( 𝑒 = 0 ↔ 𝑒 = ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 ) ) ) )
6		eleq1w	⊢ ( 𝑦 = 𝑒 → ( 𝑦 ∈ 𝐵 ↔ 𝑒 ∈ 𝐵 ) )
7		oveq1	⊢ ( 𝑦 = 𝑒 → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) )
8	7	eqeq1d	⊢ ( 𝑦 = 𝑒 → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ↔ ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ) )
9	8	ovanraleqv	⊢ ( 𝑦 = 𝑒 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
10	6 9	anbi12d	⊢ ( 𝑦 = 𝑒 → ( ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 ) ) ↔ ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) ) )
11	10	iotan0	⊢ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 ≠ ∅ ∧ 𝑒 = ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 ) ) ) ) → ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
12		rsp	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) → ( 𝑥 ∈ 𝐵 → ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
13	11 12	simpl2im	⊢ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 ≠ ∅ ∧ 𝑒 = ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝐵 → ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
14	13	3expb	⊢ ( ( 𝑒 ∈ 𝐵 ∧ ( 𝑒 ≠ ∅ ∧ 𝑒 = ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 ) ) ) ) ) → ( 𝑥 ∈ 𝐵 → ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
15	14	expcom	⊢ ( ( 𝑒 ≠ ∅ ∧ 𝑒 = ( ℩ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 ) ) ) ) → ( 𝑒 ∈ 𝐵 → ( 𝑥 ∈ 𝐵 → ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) ) )
16	5 15	sylan2b	⊢ ( ( 𝑒 ≠ ∅ ∧ 𝑒 = 0 ) → ( 𝑒 ∈ 𝐵 → ( 𝑥 ∈ 𝐵 → ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) ) )
17	16	impcom	⊢ ( ( 𝑒 ∈ 𝐵 ∧ ( 𝑒 ≠ ∅ ∧ 𝑒 = 0 ) ) → ( 𝑥 ∈ 𝐵 → ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
18	17	ralrimiv	⊢ ( ( 𝑒 ∈ 𝐵 ∧ ( 𝑒 ≠ ∅ ∧ 𝑒 = 0 ) ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) )
19	18	ex	⊢ ( 𝑒 ∈ 𝐵 → ( ( 𝑒 ≠ ∅ ∧ 𝑒 = 0 ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
20	19	reximia	⊢ ( ∃ 𝑒 ∈ 𝐵 ( 𝑒 ≠ ∅ ∧ 𝑒 = 0 ) → ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) )
21	20	anim2i	⊢ ( ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ( 𝑒 ≠ ∅ ∧ 𝑒 = 0 ) ) → ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
22	1 3	ismnddef	⊢ ( 𝐺 ∈ Mnd ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑒 ) = 𝑥 ) ) )
23	21 22	sylibr	⊢ ( ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ( 𝑒 ≠ ∅ ∧ 𝑒 = 0 ) ) → 𝐺 ∈ Mnd )