HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem grpinveu 12428
Description: The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 24-Aug-2011.)
Hypotheses
Ref Expression
grpinveu.b  |-  B  =  ( Base `  G )
grpinveu.p  |-  P  =  ( +g  `  G )
grpinveu.o  |-  O  =  ( 0g `  G )
Assertion
Ref Expression
grpinveu  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  E! y  e.  B  (
y P X )  =  O )
Distinct variable groups:    y, B    y, G    y, P    y, O    y, X

Proof of Theorem grpinveu
StepHypRef Expression
1 grpinveu.b . . . 4  |-  B  =  ( Base `  G )
2 grpinveu.p . . . 4  |-  P  =  ( +g  `  G )
3 grpinveu.o . . . 4  |-  O  =  ( 0g `  G )
41, 2, 3grpinvex 12409 . . 3  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  E. y  e.  B  ( y P X )  =  O )
5 eqtr3 2101 . . . . . . . . . . . 12  |-  ( (
( y P X )  =  O  /\  ( z P X )  =  O )  ->  ( y P X )  =  ( z P X ) )
61, 2grprcan 12427 . . . . . . . . . . . 12  |-  ( ( G  e.  Grp  /\  (
y  e.  B  /\  z  e.  B  /\  X  e.  B )
)  ->  ( (
y P X )  =  ( z P X )  <->  y  =  z ) )
75, 6syl5ib 208 . . . . . . . . . . 11  |-  ( ( G  e.  Grp  /\  (
y  e.  B  /\  z  e.  B  /\  X  e.  B )
)  ->  ( (
( y P X )  =  O  /\  ( z P X )  =  O )  ->  y  =  z ) )
873exp2 1137 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  ( y  e.  B  ->  ( z  e.  B  ->  ( X  e.  B  ->  ( ( ( y P X )  =  O  /\  ( z P X )  =  O )  ->  y  =  z ) ) ) ) )
98com24 81 . . . . . . . . 9  |-  ( G  e.  Grp  ->  ( X  e.  B  ->  ( z  e.  B  ->  (
y  e.  B  -> 
( ( ( y P X )  =  O  /\  ( z P X )  =  O )  ->  y  =  z ) ) ) ) )
109imp41 571 . . . . . . . 8  |-  ( (
( ( G  e. 
Grp  /\  X  e.  B )  /\  z  e.  B )  /\  y  e.  B )  ->  (
( ( y P X )  =  O  /\  ( z P X )  =  O )  ->  y  =  z ) )
1110an32s 741 . . . . . . 7  |-  ( (
( ( G  e. 
Grp  /\  X  e.  B )  /\  y  e.  B )  /\  z  e.  B )  ->  (
( ( y P X )  =  O  /\  ( z P X )  =  O )  ->  y  =  z ) )
1211exp3a 422 . . . . . 6  |-  ( (
( ( G  e. 
Grp  /\  X  e.  B )  /\  y  e.  B )  /\  z  e.  B )  ->  (
( y P X )  =  O  -> 
( ( z P X )  =  O  ->  y  =  z ) ) )
1312ralrimdva 2372 . . . . 5  |-  ( (
( G  e.  Grp  /\  X  e.  B )  /\  y  e.  B
)  ->  ( (
y P X )  =  O  ->  A. z  e.  B  ( (
z P X )  =  O  ->  y  =  z ) ) )
1413ancld 532 . . . 4  |-  ( (
( G  e.  Grp  /\  X  e.  B )  /\  y  e.  B
)  ->  ( (
y P X )  =  O  ->  (
( y P X )  =  O  /\  A. z  e.  B  ( ( z P X )  =  O  -> 
y  =  z ) ) ) )
1514reximdva 2394 . . 3  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( E. y  e.  B  ( y P X )  =  O  ->  E. y  e.  B  ( ( y P X )  =  O  /\  A. z  e.  B  ( ( z P X )  =  O  ->  y  =  z ) ) ) )
164, 15mpd 14 . 2  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  E. y  e.  B  ( (
y P X )  =  O  /\  A. z  e.  B  (
( z P X )  =  O  -> 
y  =  z ) ) )
17 oveq1 5361 . . . 4  |-  ( y  =  z  ->  ( y P X )  =  ( z P X ) )
1817eqeq1d 2090 . . 3  |-  ( y  =  z  ->  ( ( y P X )  =  O  <->  ( z P X )  =  O ) )
1918reu8 2663 . 2  |-  ( E! y  e.  B  (
y P X )  =  O  <->  E. y  e.  B  ( (
y P X )  =  O  /\  A. z  e.  B  (
( z P X )  =  O  -> 
y  =  z ) ) )
2016, 19sylibr 201 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  E! y  e.  B  (
y P X )  =  O )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 357    /\ w3a 903    = wceq 1536    e. wcel 1538   A.wral 2291   E.wrex 2292   E!wreu 2293   ` cfv 4287  (class class class)co 5354   Basecbs 11602   +g cplusg 11655   0gc0g 11828   Grpcgrp 12197
This theorem is referenced by:  grpinvf  12439  grplinv  12441  isgrpinv  12445
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-13 1542  ax-14 1543  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-sep 3715  ax-nul 3723  ax-pr 3783  ax-un 4075
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 905  df-ex 1456  df-sb 1754  df-eu 1976  df-mo 1977  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-ral 2295  df-rex 2296  df-reu 2297  df-rab 2298  df-v 2494  df-sbc 2668  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3089  df-if 3199  df-sn 3278  df-pr 3279  df-op 3281  df-uni 3439  df-br 3601  df-opab 3655  df-mpt 3656  df-id 3874  df-xp 4289  df-rel 4290  df-cnv 4291  df-co 4292  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fun 4297  df-fv 4303  df-ov 5357  df-iota 5762  df-0g 11832  df-mnd 12202  df-grp 12401
Copyright terms: Public domain