Theorem ismnddef

Description: The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009) (Revised by AV, 1-Feb-2020)

	Ref	Expression
Hypotheses	ismnddef.b	$$⊢B={\mathrm{Base}}_G$$
	ismnddef.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	ismnddef	$$⊢G\in \mathrm{Mnd}\leftrightarrow \left(G\in \mathrm{Smgrp}\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		ismnddef.b	$$⊢B={\mathrm{Base}}_G$$
2		ismnddef.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		fvex	$$⊢{\mathrm{Base}}_g\in \mathrm{V}$$
4		fvex	$$⊢{+}_g\in \mathrm{V}$$
5		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
6	5 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=B$$
7	6	eqeq2d	$$⊢g=G\to \left(b={\mathrm{Base}}_g\leftrightarrow b=B\right)$$
8		fveq2	$$⊢g=G\to {+}_g={+}_G$$
9	8 2	eqtr4di	$$⊢g=G\to {+}_g=\underset{\dot{}}{+}$$
10	9	eqeq2d	$$⊢g=G\to \left(p={+}_g\leftrightarrow p=\underset{\dot{}}{+}\right)$$
11	7 10	anbi12d	$$⊢g=G\to \left(\left(b={\mathrm{Base}}_g\wedge p={+}_g\right)\leftrightarrow \left(b=B\wedge p=\underset{\dot{}}{+}\right)\right)$$
12		simpl	$$⊢\left(b=B\wedge p=\underset{\dot{}}{+}\right)\to b=B$$
13		oveq	$$⊢p=\underset{\dot{}}{+}\to epa=e\underset{\dot{}}{+}a$$
14	13	eqeq1d	$$⊢p=\underset{\dot{}}{+}\to \left(epa=a\leftrightarrow e\underset{\dot{}}{+}a=a\right)$$
15		oveq	$$⊢p=\underset{\dot{}}{+}\to ape=a\underset{\dot{}}{+}e$$
16	15	eqeq1d	$$⊢p=\underset{\dot{}}{+}\to \left(ape=a\leftrightarrow a\underset{\dot{}}{+}e=a\right)$$
17	14 16	anbi12d	$$⊢p=\underset{\dot{}}{+}\to \left(\left(epa=a\wedge ape=a\right)\leftrightarrow \left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)$$
18	17	adantl	$$⊢\left(b=B\wedge p=\underset{\dot{}}{+}\right)\to \left(\left(epa=a\wedge ape=a\right)\leftrightarrow \left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)$$
19	12 18	raleqbidv	$$⊢\left(b=B\wedge p=\underset{\dot{}}{+}\right)\to \left(\forall a\in b\left(epa=a\wedge ape=a\right)\leftrightarrow \forall a\in B\left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)$$
20	12 19	rexeqbidv	$$⊢\left(b=B\wedge p=\underset{\dot{}}{+}\right)\to \left(\exists e\in b\forall a\in b\left(epa=a\wedge ape=a\right)\leftrightarrow \exists e\in B\forall a\in B\left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)$$
21	11 20	biimtrdi	$$⊢g=G\to \left(\left(b={\mathrm{Base}}_g\wedge p={+}_g\right)\to \left(\exists e\in b\forall a\in b\left(epa=a\wedge ape=a\right)\leftrightarrow \exists e\in B\forall a\in B\left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)\right)$$
22	3 4 21	sbc2iedv	$$⊢g=G\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/p\underset{\dot{}}{]}\exists e\in b\forall a\in b\left(epa=a\wedge ape=a\right)\leftrightarrow \exists e\in B\forall a\in B\left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)$$
23		df-mnd	$$⊢\mathrm{Mnd}=\left\{g\in \mathrm{Smgrp}|\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/p\underset{\dot{}}{]}\exists e\in b\forall a\in b\left(epa=a\wedge ape=a\right)\right\}$$
24	22 23	elrab2	$$⊢G\in \mathrm{Mnd}\leftrightarrow \left(G\in \mathrm{Smgrp}\wedge \exists e\in B\forall a\in B\left(e\underset{\dot{}}{+}a=a\wedge a\underset{\dot{}}{+}e=a\right)\right)$$