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

Theorem grpinveu 11718
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 11700 . . 3
5 eqtr3 2049 . . . . . . . . . . . 12
61, 2grprcan 11717 . . . . . . . . . . . 12
75, 6syl5ib 208 . . . . . . . . . . 11
873exp2 1130 . . . . . . . . . 10
98com24 81 . . . . . . . . 9
109imp41 570 . . . . . . . 8
1110an32s 741 . . . . . . 7
1211exp3a 421 . . . . . 6
1312ralrimdva 2320 . . . . 5
1413ancld 531 . . . 4
1514reximdva 2342 . . 3
164, 15mpd 14 . 2
17 oveq1 5211 . . . 4
1817eqeq1d 2038 . . 3
1918reu8 2605 . 2
2016, 19sylibr 201 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   w3a 899   wceq 1526   wcel 1528  wral 2239  wrex 2240  wreu 2241  cfv 4184  (class class class)co 5206  cbs 11159   cplusg 11199  cgrp 11617  c0g 11618
This theorem is referenced by:  grpinvf 11729  grplinv 11731  isgrpinv 11735
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-13 1534  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-sep 3626  ax-nul 3635  ax-pr 3695  ax-un 3973
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-reu 2245  df-rab 2246  df-v 2442  df-sbc 2609  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-nul 3026  df-if 3135  df-sn 3214  df-pr 3215  df-op 3217  df-uni 3375  df-br 3532  df-opab 3585  df-id 3787  df-xp 4186  df-rel 4187  df-cnv 4188  df-co 4189  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fun 4194  df-fv 4200  df-ov 5208  df-mpt 5371  df-iota 5647  df-riota 6281  df-mnd 11622  df-0g 11623  df-grp 11692
Copyright terms: Public domain