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

Theorem grpinvop 10716
 Description: The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55.
Hypotheses
Ref Expression
grpasscan1.1
grpasscan1.2 inv
Assertion
Ref Expression
grpinvop GrpOp

Proof of Theorem grpinvop
StepHypRef Expression
1 simp1 1100 . . . 4 GrpOp GrpOp
2 simp2 1101 . . . 4 GrpOp
3 simp3 1102 . . . 4 GrpOp
4 grpasscan1.1 . . . . . . 7
5 grpasscan1.2 . . . . . . 7 inv
64, 5grpoinvcl 10703 . . . . . 6 GrpOp
763adant2 1119 . . . . 5 GrpOp
84, 5grpoinvcl 10703 . . . . . 6 GrpOp
983adant3 1120 . . . . 5 GrpOp
104grpocl 10675 . . . . 5 GrpOp
111, 7, 9, 10syl111anc 1323 . . . 4 GrpOp
124grpoass 10678 . . . 4 GrpOp
131, 2, 3, 11, 12syl13anc 1325 . . 3 GrpOp
14 eqid 2136 . . . . . . . 8 Id Id
154, 14, 5grporinv 10706 . . . . . . 7 GrpOp Id
16153adant2 1119 . . . . . 6 GrpOp Id
1716opreq1d 5075 . . . . 5 GrpOp Id
184grpoass 10678 . . . . . 6 GrpOp
191, 3, 7, 9, 18syl13anc 1325 . . . . 5 GrpOp
204, 14grpolid 10696 . . . . . . 7 GrpOp Id
218, 20syldan 661 . . . . . 6 GrpOp Id
22213adant3 1120 . . . . 5 GrpOp Id
2317, 19, 223eqtr3d 2176 . . . 4 GrpOp
2423opreq2d 5076 . . 3 GrpOp
254, 14, 5grporinv 10706 . . . 4 GrpOp Id
26253adant3 1120 . . 3 GrpOp Id
2713, 24, 263eqtrd 2172 . 2 GrpOp Id
284grpocl 10675 . . 3 GrpOp
294, 14, 5grpoinvid1 10707 . . 3 GrpOp Id
301, 28, 11, 29syl111anc 1323 . 2 GrpOp Id
3127, 30mpbird 273 1 GrpOp
 Colors of variables: wff set class Syntax hints:   wi 3   wb 214   w3a 1082   wceq 1560   wcel 1562   crn 4160  cfv 4171  (class class class)co 5063  GrpOpcgr 10659  Idcgi 10660  invcgn 10661 This theorem is referenced by:  grpinvdiv 10720  grppnpcan2 10728  gxcom 10743  gxinv 10744  gxsuc 10746  gxdi 10773  ablinvop 14808  invaddvec 14922 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1564  ax-6 1565  ax-7 1566  ax-gen 1567  ax-8 1638  ax-10 1639  ax-11 1640  ax-12 1641  ax-13 1642  ax-14 1643  ax-17 1650  ax-9 1661  ax-4 1666  ax-10o 1778  ax-16 1846  ax-11o 1857  ax-ext 2118  ax-rep 3627  ax-sep 3637  ax-nul 3647  ax-pow 3683  ax-pr 3707  ax-un 3969 This theorem depends on definitions:  df-bi 215  df-or 418  df-an 419  df-3an 1084  df-ex 1569  df-sb 1808  df-eu 2036  df-mo 2037  df-clab 2124  df-cleq 2129  df-clel 2132  df-ne 2264  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2361  df-v 2545  df-sbc 2713  df-csb 2786  df-dif 2844  df-un 2846  df-in 2848  df-ss 2850  df-nul 3101  df-if 3201  df-pw 3253  df-sn 3268  df-pr 3269  df-op 3272  df-uni 3396  df-br 3538  df-opab 3596  df-id 3787  df-xp 4173  df-rel 4174  df-cnv 4175  df-co 4176  df-dm 4177  df-rn 4178  df-res 4179  df-ima 4180  df-fun 4181  df-fn 4182  df-f 4183  df-f1 4184  df-fo 4185  df-f1o 4186  df-fv 4187  df-opr 5065  df-grpo 10664  df-gid 10665  df-ginv 10666