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

Theorem grpinveu 10630
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 10612 . . 3
5 eqtr3 1937 . . . . . . . . . . . 12
61, 2grprcan 10629 . . . . . . . . . . . 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 4984 . . . 4
1817eqeq1d 1926 . . 3
1918reu8 2489 . 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 4019  (class class class)co 4979  cbs 10204   cplusg 10239  cgrp 10564  c0g 10565
This theorem is referenced by:  grpinvcl 10638  grplinv 10639  isgrpinv 10643
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 3466  ax-nul 3475  ax-pr 3535  ax-un 3809
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 2326  df-sbc 2493  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-nul 2903  df-if 3009  df-sn 3085  df-pr 3086  df-op 3088  df-uni 3224  df-br 3371  df-opab 3425  df-id 3623  df-xp 4021  df-rel 4022  df-cnv 4023  df-co 4024  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fun 4029  df-fv 4035  df-ov 4981  df-mpt 5142  df-iota 5377  df-riota 5951  df-mnd 10569  df-0g 10570  df-grp 10604
Copyright terms: Public domain