grpoideu

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

		Ref	Expression
	Hypothesis	grpfo.1	$⊢ X = ran G$
	Assertion	grpoideu	$⊢ G \in GrpOp \to \exists! u \in X \forall x \in X u G x = x$

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	$⊢ X = ran G$
2	1	grpoidinv	$⊢ G \in GrpOp \to \exists u \in X \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))$
3		simpll	$⊢ ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u)) \to u G z = z$
4	3	ralimi	$⊢ \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u)) \to \forall z \in X u G z = z$
5		oveq2	$⊢ z = x \to u G z = u G x$
6		id	$⊢ z = x \to z = x$
7	5 6	eqeq12d	$⊢ z = x \to (u G z = z \leftrightarrow u G x = x)$
8	7	cbvralvw	$⊢ \forall z \in X u G z = z \leftrightarrow \forall x \in X u G x = x$
9	4 8	sylib	$⊢ \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u)) \to \forall x \in X u G x = x$
10	9	adantl	$⊢ ((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \to \forall x \in X u G x = x$
11	9	ad2antlr	$⊢ (((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \to \forall x \in X u G x = x$
12		simpr	$⊢ ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u)) \to \exists y \in X (y G z = u \land z G y = u)$
13	12	ralimi	$⊢ \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u)) \to \forall z \in X \exists y \in X (y G z = u \land z G y = u)$
14		oveq2	$⊢ z = w \to y G z = y G w$
15	14	eqeq1d	$⊢ z = w \to (y G z = u \leftrightarrow y G w = u)$
16		oveq1	$⊢ z = w \to z G y = w G y$
17	16	eqeq1d	$⊢ z = w \to (z G y = u \leftrightarrow w G y = u)$
18	15 17	anbi12d	$⊢ z = w \to ((y G z = u \land z G y = u) \leftrightarrow (y G w = u \land w G y = u))$
19	18	rexbidv	$⊢ z = w \to (\exists y \in X (y G z = u \land z G y = u) \leftrightarrow \exists y \in X (y G w = u \land w G y = u))$
20	19	rspcva	$⊢ (w \in X \land \forall z \in X \exists y \in X (y G z = u \land z G y = u)) \to \exists y \in X (y G w = u \land w G y = u)$
21	20	adantll	$⊢ ((G \in GrpOp \land w \in X) \land \forall z \in X \exists y \in X (y G z = u \land z G y = u)) \to \exists y \in X (y G w = u \land w G y = u)$
22	13 21	sylan2	$⊢ ((G \in GrpOp \land w \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \to \exists y \in X (y G w = u \land w G y = u)$
23	1	grpoidinvlem4	$⊢ ((G \in GrpOp \land w \in X) \land \exists y \in X (y G w = u \land w G y = u)) \to w G u = u G w$
24	22 23	syldan	$⊢ ((G \in GrpOp \land w \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \to w G u = u G w$
25	24	an32s	$⊢ ((G \in GrpOp \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \to w G u = u G w$
26	25	adantllr	$⊢ (((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \to w G u = u G w$
27	26	adantr	$⊢ ((((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \land (\forall x \in X u G x = x \land \forall x \in X w G x = x)) \to w G u = u G w$
28		oveq2	$⊢ x = u \to w G x = w G u$
29		id	$⊢ x = u \to x = u$
30	28 29	eqeq12d	$⊢ x = u \to (w G x = x \leftrightarrow w G u = u)$
31	30	rspcva	$⊢ (u \in X \land \forall x \in X w G x = x) \to w G u = u$
32	31	adantll	$⊢ ((G \in GrpOp \land u \in X) \land \forall x \in X w G x = x) \to w G u = u$
33	32	ad2ant2rl	$⊢ (((G \in GrpOp \land u \in X) \land w \in X) \land (\forall x \in X u G x = x \land \forall x \in X w G x = x)) \to w G u = u$
34	33	adantllr	$⊢ ((((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \land (\forall x \in X u G x = x \land \forall x \in X w G x = x)) \to w G u = u$
35		oveq2	$⊢ x = w \to u G x = u G w$
36		id	$⊢ x = w \to x = w$
37	35 36	eqeq12d	$⊢ x = w \to (u G x = x \leftrightarrow u G w = w)$
38	37	rspcva	$⊢ (w \in X \land \forall x \in X u G x = x) \to u G w = w$
39	38	ad2ant2lr	$⊢ ((((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \land (\forall x \in X u G x = x \land \forall x \in X w G x = x)) \to u G w = w$
40	27 34 39	3eqtr3d	$⊢ ((((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \land (\forall x \in X u G x = x \land \forall x \in X w G x = x)) \to u = w$
41	40	ex	$⊢ (((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \to ((\forall x \in X u G x = x \land \forall x \in X w G x = x) \to u = w)$
42	11 41	mpand	$⊢ (((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \land w \in X) \to (\forall x \in X w G x = x \to u = w)$
43	42	ralrimiva	$⊢ ((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \to \forall w \in X (\forall x \in X w G x = x \to u = w)$
44	10 43	jca	$⊢ ((G \in GrpOp \land u \in X) \land \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u))) \to (\forall x \in X u G x = x \land \forall w \in X (\forall x \in X w G x = x \to u = w))$
45	44	ex	$⊢ (G \in GrpOp \land u \in X) \to (\forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u)) \to (\forall x \in X u G x = x \land \forall w \in X (\forall x \in X w G x = x \to u = w)))$
46	45	reximdva	$⊢ G \in GrpOp \to (\exists u \in X \forall z \in X ((u G z = z \land z G u = z) \land \exists y \in X (y G z = u \land z G y = u)) \to \exists u \in X (\forall x \in X u G x = x \land \forall w \in X (\forall x \in X w G x = x \to u = w)))$
47	2 46	mpd	$⊢ G \in GrpOp \to \exists u \in X (\forall x \in X u G x = x \land \forall w \in X (\forall x \in X w G x = x \to u = w))$
48		oveq1	$⊢ u = w \to u G x = w G x$
49	48	eqeq1d	$⊢ u = w \to (u G x = x \leftrightarrow w G x = x)$
50	49	ralbidv	$⊢ u = w \to (\forall x \in X u G x = x \leftrightarrow \forall x \in X w G x = x)$
51	50	reu8	$⊢ \exists! u \in X \forall x \in X u G x = x \leftrightarrow \exists u \in X (\forall x \in X u G x = x \land \forall w \in X (\forall x \in X w G x = x \to u = w))$
52	47 51	sylibr	$⊢ G \in GrpOp \to \exists! u \in X \forall x \in X u G x = x$

Metamath Proof Explorer

Theorem grpoideu

Proof