# Metamath Proof Explorer

## Theorem 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 e. GrpOp /\ A e. X ) -> E! y e. 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 e. GrpOp /\ A e. X ) -> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) )`
4 simpl
` |-  ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U )`
5 4 reximi
` |-  ( E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) -> E. y e. X ( y G A ) = U )`
` |-  ( ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) -> E. y e. X ( y G A ) = U )`
7 3 6 syl
` |-  ( ( G e. GrpOp /\ A e. X ) -> E. y e. X ( y G A ) = U )`
8 eqtr3
` |-  ( ( ( y G A ) = U /\ ( z G A ) = U ) -> ( y G A ) = ( z G A ) )`
9 1 grporcan
` |-  ( ( G e. GrpOp /\ ( y e. X /\ z e. X /\ A e. X ) ) -> ( ( y G A ) = ( z G A ) <-> y = z ) )`
10 8 9 syl5ib
` |-  ( ( G e. GrpOp /\ ( y e. X /\ z e. X /\ A e. X ) ) -> ( ( ( y G A ) = U /\ ( z G A ) = U ) -> y = z ) )`
11 10 3exp2
` |-  ( G e. GrpOp -> ( y e. X -> ( z e. X -> ( A e. X -> ( ( ( y G A ) = U /\ ( z G A ) = U ) -> y = z ) ) ) ) )`
12 11 com24
` |-  ( G e. GrpOp -> ( A e. X -> ( z e. X -> ( y e. X -> ( ( ( y G A ) = U /\ ( z G A ) = U ) -> y = z ) ) ) ) )`
13 12 imp41
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ z e. X ) /\ y e. X ) -> ( ( ( y G A ) = U /\ ( z G A ) = U ) -> y = z ) )`
14 13 an32s
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) /\ z e. X ) -> ( ( ( y G A ) = U /\ ( z G A ) = U ) -> y = z ) )`
15 14 expd
` |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) /\ z e. X ) -> ( ( y G A ) = U -> ( ( z G A ) = U -> y = z ) ) )`
16 15 ralrimdva
` |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> ( ( y G A ) = U -> A. z e. X ( ( z G A ) = U -> y = z ) ) )`
17 16 ancld
` |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> ( ( y G A ) = U -> ( ( y G A ) = U /\ A. z e. X ( ( z G A ) = U -> y = z ) ) ) )`
18 17 reximdva
` |-  ( ( G e. GrpOp /\ A e. X ) -> ( E. y e. X ( y G A ) = U -> E. y e. X ( ( y G A ) = U /\ A. z e. X ( ( z G A ) = U -> y = z ) ) ) )`
19 7 18 mpd
` |-  ( ( G e. GrpOp /\ A e. X ) -> E. y e. X ( ( y G A ) = U /\ A. z e. X ( ( z G A ) = U -> y = z ) ) )`
20 oveq1
` |-  ( y = z -> ( y G A ) = ( z G A ) )`
21 20 eqeq1d
` |-  ( y = z -> ( ( y G A ) = U <-> ( z G A ) = U ) )`
22 21 reu8
` |-  ( E! y e. X ( y G A ) = U <-> E. y e. X ( ( y G A ) = U /\ A. z e. X ( ( z G A ) = U -> y = z ) ) )`
23 19 22 sylibr
` |-  ( ( G e. GrpOp /\ A e. X ) -> E! y e. X ( y G A ) = U )`