Theorem grpideu

Description: The two-sided identity element of a group is unique. Lemma 2.2.1(a) of Herstein p. 55. (Contributed by NM, 16-Aug-2011) (Revised by Mario Carneiro, 8-Dec-2014)

	Ref	Expression
Hypotheses	grpcl.b	$$⊢B={\mathrm{Base}}_G$$
	grpcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpinvex.p	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grpideu	$$⊢G\in \mathrm{Grp}\to \exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpcl.b	$$⊢B={\mathrm{Base}}_G$$
2		grpcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpinvex.p	$$⊢\underset{\dot{}}{0}=0_G$$
4		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
5	1 2	mndideu	$$⊢G\in \mathrm{Mnd}\to \exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$
6	4 5	syl	$$⊢G\in \mathrm{Grp}\to \exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$