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

Theorem grpinveu 10544
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 10526 . . 3
5 eqtr3 1936 . . . . . . . . . . . 12
61, 2grprcan 10543 . . . . . . . . . . . 12
75, 6syl5ib 207 . . . . . . . . . . 11
873exp2 1129 . . . . . . . . . 10
98com24 80 . . . . . . . . 9
109imp41 569 . . . . . . . 8
1110an32s 740 . . . . . . 7
1211exp3a 420 . . . . . 6
1312ralrimdva 2206 . . . . 5
1413ancld 530 . . . 4
1514reximdva 2228 . . 3
164, 15mpd 13 . 2
17 oveq1 4949 . . . 4
1817eqeq1d 1925 . . 3
1918reu8 2487 . 2
2016, 19sylibr 200 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 356   w3a 898   wceq 1413   wcel 1415  wral 2125  wrex 2126  wreu 2127  cfv 4007  (class class class)co 4944  cbs 10137   cplusg 10172  cgrp 10478  c0g 10479
This theorem is referenced by:  grpinvcl 10552  grplinv 10553  isgrpinv 10557
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-sep 3454  ax-nul 3463  ax-pr 3523  ax-un 3797
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3an 900  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-nul 2899  df-if 3004  df-sn 3079  df-pr 3080  df-op 3082  df-uni 3214  df-br 3359  df-opab 3413  df-id 3611  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fv 4023  df-ov 4946  df-mpt 5106  df-iota 5336  df-riota 5896  df-mnd 10483  df-0g 10484  df-grp 10518
Copyright terms: Public domain