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

Theorem grpinveu 10272
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 . . . . 5
2 grpinveu.p . . . . 5
3 grpinveu.o . . . . 5
41, 2, 3grpidinv2 10267 . . . 4
5 simpl 440 . . . . . 6
65reximi 2236 . . . . 5
76adantl 449 . . . 4
84, 7syl 14 . . 3
9 eqtr3 1948 . . . . . . . . . . . 12
101, 2grprcan 10271 . . . . . . . . . . . 12
119, 10syl5ib 208 . . . . . . . . . . 11
12113exp2 1141 . . . . . . . . . 10
1312com24 80 . . . . . . . . 9
1413imp41 574 . . . . . . . 8
1514an32s 749 . . . . . . 7
1615exp3a 425 . . . . . 6
1716ralrimdva 2219 . . . . 5
1817ancld 535 . . . 4
1918reximdva 2241 . . 3
208, 19mpd 13 . 2
21 oveq1 4929 . . . 4
2221eqeq1d 1937 . . 3
2322reu8 2498 . 2
2420, 23sylibr 201 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 360   w3a 912   wceq 1425   wcel 1427  wral 2138  wrex 2139  wreu 2140  cfv 4003  (class class class)co 4924  cbs 10015   cplusg 10223  cgrp 10224  c0g 10225
This theorem is referenced by:  grpinvcl 10280  grpinv 10281  isgrpinv 10286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-sep 3454  ax-nul 3463  ax-pr 3523  ax-un 3795
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3an 914  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-sbc 2502  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-nul 2900  df-if 3005  df-sn 3080  df-pr 3081  df-op 3083  df-uni 3214  df-br 3359  df-opab 3413  df-id 3611  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fv 4019  df-ov 4926  df-mpt 5063  df-iota 5277  df-riota 5825  df-grp 10230  df-0g 10231
Copyright terms: Public domain