Theorem gsumvallem2

Description: Lemma for properties of the set of identities of G . The set of identities of a monoid is exactly the unique identity element. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	gsumvallem2.b	$$⊢B={\mathrm{Base}}_G$$
	gsumvallem2.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumvallem2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumvallem2.o	$$⊢O=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
Assertion	gsumvallem2	$$⊢G\in \mathrm{Mnd}\to O=\left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		gsumvallem2.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumvallem2.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumvallem2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		gsumvallem2.o	$$⊢O=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
5	1 2 3 4	mgmidsssn0	$$⊢G\in \mathrm{Mnd}\to O\subseteq \left\{\underset{\dot{}}{0}\right\}$$
6	1 2	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
7	1 3 2	mndlrid	$$⊢\left(G\in \mathrm{Mnd}\wedge y\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}\underset{\dot{}}{0}=y\right)$$
8	7	ralrimiva	$$⊢G\in \mathrm{Mnd}\to \forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}\underset{\dot{}}{0}=y\right)$$
9		oveq1	$$⊢x=\underset{\dot{}}{0}\to x\underset{\dot{}}{+}y=\underset{\dot{}}{0}\underset{\dot{}}{+}y$$
10	9	eqeq1d	$$⊢x=\underset{\dot{}}{0}\to \left(x\underset{\dot{}}{+}y=y\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{+}y=y\right)$$
11	10	ovanraleqv	$$⊢x=\underset{\dot{}}{0}\to \left(\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\leftrightarrow \forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}\underset{\dot{}}{0}=y\right)\right)$$
12	11 4	elrab2	$$⊢\underset{\dot{}}{0}\in O\leftrightarrow \left(\underset{\dot{}}{0}\in B\wedge \forall y\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}\underset{\dot{}}{0}=y\right)\right)$$
13	6 8 12	sylanbrc	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in O$$
14	13	snssd	$$⊢G\in \mathrm{Mnd}\to \left\{\underset{\dot{}}{0}\right\}\subseteq O$$
15	5 14	eqssd	$$⊢G\in \mathrm{Mnd}\to O=\left\{\underset{\dot{}}{0}\right\}$$