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

Theorem grpinveu 11906
Description: The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55.
Hypotheses
Ref Expression
grpinveu.b
grpinveu.p
grpinveu.o
Assertion
Ref Expression
grpinveu
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem grpinveu
StepHypRef Expression
1 grpinveu.b . . . 4
2 grpinveu.p . . . 4
3 grpinveu.o . . . 4
41, 2, 3grpinvex 11888 . . 3
5 eqtr3 2109 . . . . . . . . . . . 12
61, 2grprcan 11905 . . . . . . . . . . . 12
75, 6syl5ib 208 . . . . . . . . . . 11
873exp2 1133 . . . . . . . . . 10
98com24 81 . . . . . . . . 9
109imp41 570 . . . . . . . 8
1110an32s 741 . . . . . . 7
1211exp3a 421 . . . . . 6
1312ralrimdva 2380 . . . . 5
1413ancld 531 . . . 4
1514reximdva 2402 . . 3
164, 15mpd 14 . 2
17 oveq1 5301 . . . 4
1817eqeq1d 2098 . . 3
1918reu8 2665 . 2
2016, 19sylibr 201 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   w3a 899   wceq 1531   wcel 1533  wral 2299  wrex 2300  wreu 2301  cfv 4261  (class class class)co 5296  cbs 11344   cplusg 11384  cgrp 11804  c0g 11805
This theorem is referenced by:  grpinvf  11917  grplinv  11919  isgrpinv  11923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pr 3756  ax-un 4049
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3086  df-if 3195  df-sn 3274  df-pr 3275  df-op 3277  df-uni 3435  df-br 3592  df-opab 3645  df-id 3848  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fv 4277  df-ov 5298  df-mpt 5461  df-iota 5740  df-riota 6415  df-mnd 11809  df-0g 11810  df-grp 11880
Copyright terms: Public domain