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

Theorem grpinvop 10925
 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 1055 . . . 4 GrpOp GrpOp
2 simp2 1056 . . . 4 GrpOp
3 simp3 1057 . . . 4 GrpOp
4 grpasscan1.1 . . . . . . 7
5 grpasscan1.2 . . . . . . 7 inv
64, 5grpoinvcl 10912 . . . . . 6 GrpOp
763adant2 1074 . . . . 5 GrpOp
84, 5grpoinvcl 10912 . . . . . 6 GrpOp
983adant3 1075 . . . . 5 GrpOp
104grpocl 10886 . . . . 5 GrpOp
111, 7, 9, 10syl111anc 1278 . . . 4 GrpOp
124grpoass 10889 . . . 4 GrpOp
131, 2, 3, 11, 12syl13anc 1280 . . 3 GrpOp
14 eqid 2092 . . . . . . . 8 Id Id
154, 14, 5grporinv 10915 . . . . . . 7 GrpOp Id
16153adant2 1074 . . . . . 6 GrpOp Id
1716opreq1d 5079 . . . . 5 GrpOp Id
184grpoass 10889 . . . . . 6 GrpOp
191, 3, 7, 9, 18syl13anc 1280 . . . . 5 GrpOp
204, 14grpolid 10905 . . . . . . 7 GrpOp Id
218, 20syldan 521 . . . . . 6 GrpOp Id
22213adant3 1075 . . . . 5 GrpOp Id
2317, 19, 223eqtr3d 2132 . . . 4 GrpOp
2423opreq2d 5080 . . 3 GrpOp
254, 14, 5grporinv 10915 . . . 4 GrpOp Id
26253adant3 1075 . . 3 GrpOp Id
2713, 24, 263eqtrd 2128 . 2 GrpOp Id
284grpocl 10886 . . 3 GrpOp
294, 14, 5grpoinvid1 10916 . . 3 GrpOp Id
301, 28, 11, 29syl111anc 1278 . 2 GrpOp Id
3127, 30mpbird 269 1 GrpOp
 Colors of variables: wff set class Syntax hints:   wi 3   wb 209   w3a 1037   wceq 1592   wcel 1594   crn 4138  cfv 4149  (class class class)co 5067  GrpOpcgr 10870  Idcgi 10871  invcgn 10872 This theorem is referenced by:  grpinvdiv 10929  grppnpcan2 10937  gxcom 10952  gxinv 10953  gxsuc 10955  gxdi 10982  ablinvop 15195  invaddvec 15316 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-13 1600  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-rep 3599  ax-sep 3609  ax-nul 3619  ax-pr 3679  ax-un 3947 This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-reu 2316  df-rab 2317  df-v 2501  df-sbc 2671  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-nul 3066  df-if 3166  df-sn 3237  df-pr 3238  df-op 3241  df-uni 3365  df-br 3510  df-opab 3568  df-id 3765  df-xp 4151  df-rel 4152  df-cnv 4153  df-co 4154  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fun 4159  df-fn 4160  df-f 4161  df-fo 4163  df-fv 4165  df-opr 5069  df-mpt 5202  df-iota 5374  df-riota 5896  df-grpo 10875  df-gid 10876  df-ginv 10877
Copyright terms: Public domain