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 )
6 5 adantl 
 |-  ( ( ( ( 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 )