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

Theorem grpinveu 10993
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 10975 . . 3
5 eqtr3 1937 . . . . . . . . . . . 12
61, 2grprcan 10992 . . . . . . . . . . . 12
75, 6syl5ib 208 . . . . . . . . . . 11
873exp2 1130 . . . . . . . . . 10
98com24 81 . . . . . . . . 9
109imp41 570 . . . . . . . 8
1110an32s 741 . . . . . . 7
1211exp3a 421 . . . . . 6
1312ralrimdva 2208 . . . . 5
1413ancld 531 . . . 4
1514reximdva 2230 . . 3
164, 15mpd 14 . 2
17 oveq1 5037 . . . 4
1817eqeq1d 1926 . . 3
1918reu8 2492 . 2
2016, 19sylibr 201 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   w3a 899   wceq 1414   wcel 1416  wral 2127  wrex 2128  wreu 2129  cfv 4046  (class class class)co 5032  cbs 10495   cplusg 10533  cgrp 10902  c0g 10903
This theorem is referenced by:  grpinvf 11001  grplinv 11003  isgrpinv 11007
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-sep 3491  ax-nul 3500  ax-pr 3560  ax-un 3836
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2329  df-sbc 2496  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-nul 2908  df-if 3015  df-sn 3092  df-pr 3093  df-op 3095  df-uni 3247  df-br 3397  df-opab 3450  df-id 3650  df-xp 4048  df-rel 4049  df-cnv 4050  df-co 4051  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fun 4056  df-fv 4062  df-ov 5034  df-mpt 5196  df-iota 5444  df-riota 6022  df-mnd 10907  df-0g 10908  df-grp 10967
Copyright terms: Public domain