grpinveu

Description: The left inverse element of a group is unique. Lemma 2.2.1(b) of Herstein p. 55. (Contributed by NM, 24-Aug-2011)

	Ref	Expression
Hypotheses	grpinveu.b	$⊢ B = {Base}_{G}$
	grpinveu.p	$⊢ \underset{˙}{+} = +_{G}$
	grpinveu.o	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	grpinveu	$⊢ (G \in Grp \land X \in B) \to \exists! y \in B y \underset{˙}{+} X = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		grpinveu.b	$⊢ B = {Base}_{G}$
2		grpinveu.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpinveu.o	$⊢ \underset{˙}{0} = 0_{G}$
4	1 2 3	grpinvex	$⊢ (G \in Grp \land X \in B) \to \exists y \in B y \underset{˙}{+} X = \underset{˙}{0}$
5		eqtr3	$⊢ (y \underset{˙}{+} X = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}) \to y \underset{˙}{+} X = z \underset{˙}{+} X$
6	1 2	grprcan	$⊢ (G \in Grp \land (y \in B \land z \in B \land X \in B)) \to (y \underset{˙}{+} X = z \underset{˙}{+} X \leftrightarrow y = z)$
7	5 6	syl5ib	$⊢ (G \in Grp \land (y \in B \land z \in B \land X \in B)) \to ((y \underset{˙}{+} X = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}) \to y = z)$
8	7	3exp2	$⊢ G \in Grp \to (y \in B \to (z \in B \to (X \in B \to ((y \underset{˙}{+} X = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}) \to y = z))))$
9	8	com24	$⊢ G \in Grp \to (X \in B \to (z \in B \to (y \in B \to ((y \underset{˙}{+} X = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}) \to y = z))))$
10	9	imp41	$⊢ (((G \in Grp \land X \in B) \land z \in B) \land y \in B) \to ((y \underset{˙}{+} X = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}) \to y = z)$
11	10	an32s	$⊢ (((G \in Grp \land X \in B) \land y \in B) \land z \in B) \to ((y \underset{˙}{+} X = \underset{˙}{0} \land z \underset{˙}{+} X = \underset{˙}{0}) \to y = z)$
12	11	expd	$⊢ (((G \in Grp \land X \in B) \land y \in B) \land z \in B) \to (y \underset{˙}{+} X = \underset{˙}{0} \to (z \underset{˙}{+} X = \underset{˙}{0} \to y = z))$
13	12	ralrimdva	$⊢ ((G \in Grp \land X \in B) \land y \in B) \to (y \underset{˙}{+} X = \underset{˙}{0} \to \forall z \in B (z \underset{˙}{+} X = \underset{˙}{0} \to y = z))$
14	13	ancld	$⊢ ((G \in Grp \land X \in B) \land y \in B) \to (y \underset{˙}{+} X = \underset{˙}{0} \to (y \underset{˙}{+} X = \underset{˙}{0} \land \forall z \in B (z \underset{˙}{+} X = \underset{˙}{0} \to y = z)))$
15	14	reximdva	$⊢ (G \in Grp \land X \in B) \to (\exists y \in B y \underset{˙}{+} X = \underset{˙}{0} \to \exists y \in B (y \underset{˙}{+} X = \underset{˙}{0} \land \forall z \in B (z \underset{˙}{+} X = \underset{˙}{0} \to y = z)))$
16	4 15	mpd	$⊢ (G \in Grp \land X \in B) \to \exists y \in B (y \underset{˙}{+} X = \underset{˙}{0} \land \forall z \in B (z \underset{˙}{+} X = \underset{˙}{0} \to y = z))$
17		oveq1	$⊢ y = z \to y \underset{˙}{+} X = z \underset{˙}{+} X$
18	17	eqeq1d	$⊢ y = z \to (y \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow z \underset{˙}{+} X = \underset{˙}{0})$
19	18	reu8	$⊢ \exists! y \in B y \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow \exists y \in B (y \underset{˙}{+} X = \underset{˙}{0} \land \forall z \in B (z \underset{˙}{+} X = \underset{˙}{0} \to y = z))$
20	16 19	sylibr	$⊢ (G \in Grp \land X \in B) \to \exists! y \in B y \underset{˙}{+} X = \underset{˙}{0}$

Metamath Proof Explorer

Theorem grpinveu

Proof