# Metamath Proof Explorer

## Theorem 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 e. GrpOp -> E! u e. X A. x e. X ( u G x ) = x )`

### Proof

Step Hyp Ref Expression
1 grpfo.1
` |-  X = ran G`
2 1 grpoidinv
` |-  ( G e. GrpOp -> E. u e. X A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) )`
3 simpll
` |-  ( ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> ( u G z ) = z )`
4 3 ralimi
` |-  ( A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> A. z e. X ( u G z ) = z )`
5 oveq2
` |-  ( z = x -> ( u G z ) = ( u G x ) )`
6 id
` |-  ( z = x -> z = x )`
7 5 6 eqeq12d
` |-  ( z = x -> ( ( u G z ) = z <-> ( u G x ) = x ) )`
8 7 cbvralvw
` |-  ( A. z e. X ( u G z ) = z <-> A. x e. X ( u G x ) = x )`
9 4 8 sylib
` |-  ( A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> A. x e. X ( u G x ) = x )`
` |-  ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) -> A. x e. X ( u G x ) = x )`
` |-  ( ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) -> A. x e. X ( u G x ) = x )`
12 simpr
` |-  ( ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) )`
13 12 ralimi
` |-  ( A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> A. z e. X E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) )`
14 oveq2
` |-  ( z = w -> ( y G z ) = ( y G w ) )`
15 14 eqeq1d
` |-  ( z = w -> ( ( y G z ) = u <-> ( y G w ) = u ) )`
16 oveq1
` |-  ( z = w -> ( z G y ) = ( w G y ) )`
17 16 eqeq1d
` |-  ( z = w -> ( ( z G y ) = u <-> ( w G y ) = u ) )`
18 15 17 anbi12d
` |-  ( z = w -> ( ( ( y G z ) = u /\ ( z G y ) = u ) <-> ( ( y G w ) = u /\ ( w G y ) = u ) ) )`
19 18 rexbidv
` |-  ( z = w -> ( E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) <-> E. y e. X ( ( y G w ) = u /\ ( w G y ) = u ) ) )`
20 19 rspcva
` |-  ( ( w e. X /\ A. z e. X E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> E. y e. X ( ( y G w ) = u /\ ( w G y ) = u ) )`
` |-  ( ( ( G e. GrpOp /\ w e. X ) /\ A. z e. X E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> E. y e. X ( ( y G w ) = u /\ ( w G y ) = u ) )`
22 13 21 sylan2
` |-  ( ( ( G e. GrpOp /\ w e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) -> E. y e. X ( ( y G w ) = u /\ ( w G y ) = u ) )`
23 1 grpoidinvlem4
` |-  ( ( ( G e. GrpOp /\ w e. X ) /\ E. y e. X ( ( y G w ) = u /\ ( w G y ) = u ) ) -> ( w G u ) = ( u G w ) )`
24 22 23 syldan
` |-  ( ( ( G e. GrpOp /\ w e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) -> ( w G u ) = ( u G w ) )`
25 24 an32s
` |-  ( ( ( G e. GrpOp /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) -> ( w G u ) = ( u G w ) )`
` |-  ( ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) -> ( w G u ) = ( u G w ) )`
` |-  ( ( ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) /\ ( A. x e. X ( u G x ) = x /\ A. x e. X ( w G x ) = x ) ) -> ( w G u ) = ( u G w ) )`
28 oveq2
` |-  ( x = u -> ( w G x ) = ( w G u ) )`
29 id
` |-  ( x = u -> x = u )`
30 28 29 eqeq12d
` |-  ( x = u -> ( ( w G x ) = x <-> ( w G u ) = u ) )`
31 30 rspcva
` |-  ( ( u e. X /\ A. x e. X ( w G x ) = x ) -> ( w G u ) = u )`
` |-  ( ( ( G e. GrpOp /\ u e. X ) /\ A. x e. X ( w G x ) = x ) -> ( w G u ) = u )`
` |-  ( ( ( ( G e. GrpOp /\ u e. X ) /\ w e. X ) /\ ( A. x e. X ( u G x ) = x /\ A. x e. X ( w G x ) = x ) ) -> ( w G u ) = u )`
` |-  ( ( ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) /\ ( A. x e. X ( u G x ) = x /\ A. x e. X ( w G x ) = x ) ) -> ( w G u ) = u )`
35 oveq2
` |-  ( x = w -> ( u G x ) = ( u G w ) )`
36 id
` |-  ( x = w -> x = w )`
37 35 36 eqeq12d
` |-  ( x = w -> ( ( u G x ) = x <-> ( u G w ) = w ) )`
38 37 rspcva
` |-  ( ( w e. X /\ A. x e. X ( u G x ) = x ) -> ( u G w ) = w )`
` |-  ( ( ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) /\ ( A. x e. X ( u G x ) = x /\ A. x e. X ( w G x ) = x ) ) -> ( u G w ) = w )`
40 27 34 39 3eqtr3d
` |-  ( ( ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) /\ ( A. x e. X ( u G x ) = x /\ A. x e. X ( w G x ) = x ) ) -> u = w )`
41 40 ex
` |-  ( ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) -> ( ( A. x e. X ( u G x ) = x /\ A. x e. X ( w G x ) = x ) -> u = w ) )`
42 11 41 mpand
` |-  ( ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) /\ w e. X ) -> ( A. x e. X ( w G x ) = x -> u = w ) )`
43 42 ralrimiva
` |-  ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) -> A. w e. X ( A. x e. X ( w G x ) = x -> u = w ) )`
44 10 43 jca
` |-  ( ( ( G e. GrpOp /\ u e. X ) /\ A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) ) -> ( A. x e. X ( u G x ) = x /\ A. w e. X ( A. x e. X ( w G x ) = x -> u = w ) ) )`
45 44 ex
` |-  ( ( G e. GrpOp /\ u e. X ) -> ( A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> ( A. x e. X ( u G x ) = x /\ A. w e. X ( A. x e. X ( w G x ) = x -> u = w ) ) ) )`
46 45 reximdva
` |-  ( G e. GrpOp -> ( E. u e. X A. z e. X ( ( ( u G z ) = z /\ ( z G u ) = z ) /\ E. y e. X ( ( y G z ) = u /\ ( z G y ) = u ) ) -> E. u e. X ( A. x e. X ( u G x ) = x /\ A. w e. X ( A. x e. X ( w G x ) = x -> u = w ) ) ) )`
47 2 46 mpd
` |-  ( G e. GrpOp -> E. u e. X ( A. x e. X ( u G x ) = x /\ A. w e. X ( A. x e. X ( w G x ) = x -> u = w ) ) )`
48 oveq1
` |-  ( u = w -> ( u G x ) = ( w G x ) )`
49 48 eqeq1d
` |-  ( u = w -> ( ( u G x ) = x <-> ( w G x ) = x ) )`
50 49 ralbidv
` |-  ( u = w -> ( A. x e. X ( u G x ) = x <-> A. x e. X ( w G x ) = x ) )`
51 50 reu8
` |-  ( E! u e. X A. x e. X ( u G x ) = x <-> E. u e. X ( A. x e. X ( u G x ) = x /\ A. w e. X ( A. x e. X ( w G x ) = x -> u = w ) ) )`
52 47 51 sylibr
` |-  ( G e. GrpOp -> E! u e. X A. x e. X ( u G x ) = x )`