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	$$⊢B={\mathrm{Base}}_G$$
	sgrpidmnd.0	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	sgrpidmnd	$$⊢\left(G\in \mathrm{Smgrp}\wedge \exists e\in B\left(e\ne \varnothing \wedge e=\underset{\dot{}}{0}\right)\right)\to G\in \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		sgrpidmnd.b	$$⊢B={\mathrm{Base}}_G$$
2		sgrpidmnd.0	$$⊢\underset{\dot{}}{0}=0_G$$
3		eqid	$$⊢{+}_G={+}_G$$
4	1 3 2	grpidval	$$⊢\underset{\dot{}}{0}=\left(\iota y|\left(y\in B\wedge \forall x\in B\left(y{+}_{G}x=x\wedge x{+}_{G}y=x\right)\right)\right)$$
5	4	eqeq2i	$$⊢e=\underset{\dot{}}{0}\leftrightarrow e=\left(\iota y|\left(y\in B\wedge \forall x\in B\left(y{+}_{G}x=x\wedge x{+}_{G}y=x\right)\right)\right)$$
6		eleq1w	$$⊢y=e\to \left(y\in B\leftrightarrow e\in B\right)$$
7		oveq1	$$⊢y=e\to y{+}_{G}x=e{+}_{G}x$$
8	7	eqeq1d	$$⊢y=e\to \left(y{+}_{G}x=x\leftrightarrow e{+}_{G}x=x\right)$$
9	8	ovanraleqv	$$⊢y=e\to \left(\forall x\in B\left(y{+}_{G}x=x\wedge x{+}_{G}y=x\right)\leftrightarrow \forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
10	6 9	anbi12d	$$⊢y=e\to \left(\left(y\in B\wedge \forall x\in B\left(y{+}_{G}x=x\wedge x{+}_{G}y=x\right)\right)\leftrightarrow \left(e\in B\wedge \forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)\right)$$
11	10	iotan0	$$⊢\left(e\in B\wedge e\ne \varnothing \wedge e=\left(\iota y|\left(y\in B\wedge \forall x\in B\left(y{+}_{G}x=x\wedge x{+}_{G}y=x\right)\right)\right)\right)\to \left(e\in B\wedge \forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
12		rsp	$$⊢\forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\to \left(x\in B\to \left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
13	11 12	simpl2im	$$⊢\left(e\in B\wedge e\ne \varnothing \wedge e=\left(\iota y|\left(y\in B\wedge \forall x\in B\left(y{+}_{G}x=x\wedge x{+}_{G}y=x\right)\right)\right)\right)\to \left(x\in B\to \left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
14	13	3expb	$$⊢\left(e\in B\wedge \left(e\ne \varnothing \wedge e=\left(\iota y|\left(y\in B\wedge \forall x\in B\left(y{+}_{G}x=x\wedge x{+}_{G}y=x\right)\right)\right)\right)\right)\to \left(x\in B\to \left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
15	14	expcom	$$⊢\left(e\ne \varnothing \wedge e=\left(\iota y|\left(y\in B\wedge \forall x\in B\left(y{+}_{G}x=x\wedge x{+}_{G}y=x\right)\right)\right)\right)\to \left(e\in B\to \left(x\in B\to \left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)\right)$$
16	5 15	sylan2b	$$⊢\left(e\ne \varnothing \wedge e=\underset{\dot{}}{0}\right)\to \left(e\in B\to \left(x\in B\to \left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)\right)$$
17	16	impcom	$$⊢\left(e\in B\wedge \left(e\ne \varnothing \wedge e=\underset{\dot{}}{0}\right)\right)\to \left(x\in B\to \left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
18	17	ralrimiv	$$⊢\left(e\in B\wedge \left(e\ne \varnothing \wedge e=\underset{\dot{}}{0}\right)\right)\to \forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)$$
19	18	ex	$$⊢e\in B\to \left(\left(e\ne \varnothing \wedge e=\underset{\dot{}}{0}\right)\to \forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
20	19	reximia	$$⊢\exists e\in B\left(e\ne \varnothing \wedge e=\underset{\dot{}}{0}\right)\to \exists e\in B\forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)$$
21	20	anim2i	$$⊢\left(G\in \mathrm{Smgrp}\wedge \exists e\in B\left(e\ne \varnothing \wedge e=\underset{\dot{}}{0}\right)\right)\to \left(G\in \mathrm{Smgrp}\wedge \exists e\in B\forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
22	1 3	ismnddef	$$⊢G\in \mathrm{Mnd}\leftrightarrow \left(G\in \mathrm{Smgrp}\wedge \exists e\in B\forall x\in B\left(e{+}_{G}x=x\wedge x{+}_{G}e=x\right)\right)$$
23	21 22	sylibr	$$⊢\left(G\in \mathrm{Smgrp}\wedge \exists e\in B\left(e\ne \varnothing \wedge e=\underset{\dot{}}{0}\right)\right)\to G\in \mathrm{Mnd}$$