grpoinveu

Description: The left inverse element of a group is unique. Lemma 2.2.1(b) of Herstein p. 55. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpoinveu.1	$⊢ X = ran G$
	grpoinveu.2	$⊢ U = GId (G)$
Assertion	grpoinveu	$⊢ (G \in GrpOp \land A \in X) \to \exists! y \in X y G A = U$

Proof

Step	Hyp	Ref	Expression
1		grpoinveu.1	$⊢ X = ran G$
2		grpoinveu.2	$⊢ U = GId (G)$
3	1 2	grpoidinv2	$⊢ (G \in GrpOp \land A \in X) \to ((U G A = A \land A G U = A) \land \exists y \in X (y G A = U \land A G y = U))$
4		simpl	$⊢ (y G A = U \land A G y = U) \to y G A = U$
5	4	reximi	$⊢ \exists y \in X (y G A = U \land A G y = U) \to \exists y \in X y G A = U$
6	5	adantl	$⊢ ((U G A = A \land A G U = A) \land \exists y \in X (y G A = U \land A G y = U)) \to \exists y \in X y G A = U$
7	3 6	syl	$⊢ (G \in GrpOp \land A \in X) \to \exists y \in X y G A = U$
8		eqtr3	$⊢ (y G A = U \land z G A = U) \to y G A = z G A$
9	1	grporcan	$⊢ (G \in GrpOp \land (y \in X \land z \in X \land A \in X)) \to (y G A = z G A \leftrightarrow y = z)$
10	8 9	imbitrid	$⊢ (G \in GrpOp \land (y \in X \land z \in X \land A \in X)) \to ((y G A = U \land z G A = U) \to y = z)$
11	10	3exp2	$⊢ G \in GrpOp \to (y \in X \to (z \in X \to (A \in X \to ((y G A = U \land z G A = U) \to y = z))))$
12	11	com24	$⊢ G \in GrpOp \to (A \in X \to (z \in X \to (y \in X \to ((y G A = U \land z G A = U) \to y = z))))$
13	12	imp41	$⊢ (((G \in GrpOp \land A \in X) \land z \in X) \land y \in X) \to ((y G A = U \land z G A = U) \to y = z)$
14	13	an32s	$⊢ (((G \in GrpOp \land A \in X) \land y \in X) \land z \in X) \to ((y G A = U \land z G A = U) \to y = z)$
15	14	expd	$⊢ (((G \in GrpOp \land A \in X) \land y \in X) \land z \in X) \to (y G A = U \to (z G A = U \to y = z))$
16	15	ralrimdva	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to (y G A = U \to \forall z \in X (z G A = U \to y = z))$
17	16	ancld	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to (y G A = U \to (y G A = U \land \forall z \in X (z G A = U \to y = z)))$
18	17	reximdva	$⊢ (G \in GrpOp \land A \in X) \to (\exists y \in X y G A = U \to \exists y \in X (y G A = U \land \forall z \in X (z G A = U \to y = z)))$
19	7 18	mpd	$⊢ (G \in GrpOp \land A \in X) \to \exists y \in X (y G A = U \land \forall z \in X (z G A = U \to y = z))$
20		oveq1	$⊢ y = z \to y G A = z G A$
21	20	eqeq1d	$⊢ y = z \to (y G A = U \leftrightarrow z G A = U)$
22	21	reu8	$⊢ \exists! y \in X y G A = U \leftrightarrow \exists y \in X (y G A = U \land \forall z \in X (z G A = U \to y = z))$
23	19 22	sylibr	$⊢ (G \in GrpOp \land A \in X) \to \exists! y \in X y G A = U$

Metamath Proof Explorer

Theorem grpoinveu

Proof