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

Metamath Proof Explorer

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 )