Theorem ismnd

Description: The predicate "is a monoid". This is the definig 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={\mathrm{Base}}_G$$
	ismnd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	ismnd	$$⊢G\in \mathrm{Mnd}\leftrightarrow \left(\forall a\in B\forall b\in B\left(a\underset{\dot{}}{+}b\in B\wedge \forall c\in B\left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{+}c=a\underset{\dot{}}{+}\left(b\underset{\dot{}}{+}c\right)\right)\wedge \exists e\in B\forall a\in B\left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismnd.b	$$⊢B={\mathrm{Base}}_G$$
2		ismnd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3	1 2	ismnddef	Could not format ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) ) : No typesetting found for |- ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) ) with typecode |-
4		rexn0	$$⊢\exists e\in B\forall a\in B\left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\to B\ne \varnothing$$
5		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
6	1 5	syl5eq	$$⊢\neg G\in \mathrm{V}\to B=\varnothing$$
7	6	necon1ai	$$⊢B\ne \varnothing \to G\in \mathrm{V}$$
8	1 2	issgrpv	Could not format ( G e. _V -> ( G e. Smgrp <-> A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) ) ) : No typesetting found for |- ( G e. _V -> ( G e. Smgrp <-> A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) ) ) with typecode |-
9	4 7 8	3syl	Could not format ( E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) -> ( G e. Smgrp <-> A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) ) ) : No typesetting found for |- ( E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) -> ( G e. Smgrp <-> A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) ) ) with typecode |-
10	9	pm5.32ri	Could not format ( ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) <-> ( A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) <-> ( A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) ) with typecode |-
11	3 10	bitri	$$⊢G\in \mathrm{Mnd}\leftrightarrow \left(\forall a\in B\forall b\in B\left(a\underset{\dot{}}{+}b\in B\wedge \forall c\in B\left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{+}c=a\underset{\dot{}}{+}\left(b\underset{\dot{}}{+}c\right)\right)\wedge \exists e\in B\forall a\in B\left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)$$