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

Theorem grpinveu 10778
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 10760 . . 3
5 eqtr3 1937 . . . . . . . . . . . 12
61, 2grprcan 10777 . . . . . . . . . . . 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 5007 . . . 4
1817eqeq1d 1926 . . 3
1918reu8 2491 . 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 4033  (class class class)co 5002  cbs 10303   cplusg 10338  cgrp 10709  c0g 10710
This theorem is referenced by:  grpinvcl 10786  grplinv 10787  isgrpinv 10791
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 3479  ax-nul 3488  ax-pr 3548  ax-un 3823
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 2328  df-sbc 2495  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-nul 2905  df-if 3012  df-sn 3089  df-pr 3090  df-op 3092  df-uni 3234  df-br 3384  df-opab 3438  df-id 3637  df-xp 4035  df-rel 4036  df-cnv 4037  df-co 4038  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fun 4043  df-fv 4049  df-ov 5004  df-mpt 5165  df-iota 5407  df-riota 5987  df-mnd 10714  df-0g 10715  df-grp 10752
Copyright terms: Public domain