Metamath Proof Explorer


Theorem ismnd

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