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 )
10 9 adantl 
 |-  ( ( ( 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 )
11 9 ad2antlr 
 |-  ( ( ( ( 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 ) )
21 20 adantll 
 |-  ( ( ( 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 ) )
26 25 adantllr 
 |-  ( ( ( ( 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 ) )
27 26 adantr 
 |-  ( ( ( ( ( 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 )
32 31 adantll 
 |-  ( ( ( G e. GrpOp /\ u e. X ) /\ A. x e. X ( w G x ) = x ) -> ( w G u ) = u )
33 32 ad2ant2rl 
 |-  ( ( ( ( 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 )
34 33 adantllr 
 |-  ( ( ( ( ( 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 )
39 38 ad2ant2lr 
 |-  ( ( ( ( ( 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 )