Database
BASIC ALGEBRAIC STRUCTURES
Monoids
Definition and basic properties of monoids
ismnd
Metamath Proof Explorer
Description: The predicate "is a monoid". This is the defining theorem of a monoid
by showing that a set is a monoid if and only if it is a set equipped
with a closed, everywhere defined internal operation (so, a magma, see
mndcl ), whose operation is associative (so, a semigroup, see also
mndass ) and has a two-sided neutral element (see mndid ).
(Contributed by Mario Carneiro , 6-Jan-2015) (Revised by AV , 1-Feb-2020)
Ref
Expression
Hypotheses
ismnd.b
⊢ B = Base G
ismnd.p
⊢ + ˙ = + G
Assertion
ismnd
⊢ G ∈ Mnd ↔ ∀ a ∈ B ∀ b ∈ B a + ˙ b ∈ B ∧ ∀ c ∈ B a + ˙ b + ˙ c = a + ˙ b + ˙ c ∧ ∃ e ∈ B ∀ a ∈ B e + ˙ a = a ∧ a + ˙ e = a
Proof
Step
Hyp
Ref
Expression
1
ismnd.b
⊢ B = Base G
2
ismnd.p
⊢ + ˙ = + G
3
1 2
ismnddef
⊢ G ∈ Mnd ↔ G ∈ Smgrp ∧ ∃ e ∈ B ∀ a ∈ B e + ˙ a = a ∧ a + ˙ e = a
4
rexn0
⊢ ∃ e ∈ B ∀ a ∈ B e + ˙ a = a ∧ a + ˙ e = a → B ≠ ∅
5
fvprc
⊢ ¬ G ∈ V → Base G = ∅
6
1 5
eqtrid
⊢ ¬ G ∈ V → B = ∅
7
6
necon1ai
⊢ B ≠ ∅ → G ∈ V
8
1 2
issgrpv
⊢ G ∈ V → G ∈ Smgrp ↔ ∀ a ∈ B ∀ b ∈ B a + ˙ b ∈ B ∧ ∀ c ∈ B a + ˙ b + ˙ c = a + ˙ b + ˙ c
9
4 7 8
3syl
⊢ ∃ e ∈ B ∀ a ∈ B e + ˙ a = a ∧ a + ˙ e = a → G ∈ Smgrp ↔ ∀ a ∈ B ∀ b ∈ B a + ˙ b ∈ B ∧ ∀ c ∈ B a + ˙ b + ˙ c = a + ˙ b + ˙ c
10
9
pm5.32ri
⊢ G ∈ Smgrp ∧ ∃ e ∈ B ∀ a ∈ B e + ˙ a = a ∧ a + ˙ e = a ↔ ∀ a ∈ B ∀ b ∈ B a + ˙ b ∈ B ∧ ∀ c ∈ B a + ˙ b + ˙ c = a + ˙ b + ˙ c ∧ ∃ e ∈ B ∀ a ∈ B e + ˙ a = a ∧ a + ˙ e = a
11
3 10
bitri
⊢ G ∈ Mnd ↔ ∀ a ∈ B ∀ b ∈ B a + ˙ b ∈ B ∧ ∀ c ∈ B a + ˙ b + ˙ c = a + ˙ b + ˙ c ∧ ∃ e ∈ B ∀ a ∈ B e + ˙ a = a ∧ a + ˙ e = a