This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Base}_{G}$
	grpcl.p	$⊢ \underset{˙}{+} = +_{G}$
	grpinvex.p	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	grpideu	$⊢ G \in Grp \to \exists! u \in B \forall x \in B (u \underset{˙}{+} x = x \land x \underset{˙}{+} u = x)$

Proof

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