Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpinvadd Structured version   Unicode version

 Description: The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.)
Hypotheses
Ref Expression
Assertion
Ref Expression

StepHypRef Expression
1 simp1 996 . . . 4
2 simp2 997 . . . 4
3 simp3 998 . . . 4
4 grpinvadd.b . . . . . . 7
5 grpinvadd.n . . . . . . 7
64, 5grpinvcl 15967 . . . . . 6
763adant2 1015 . . . . 5
84, 5grpinvcl 15967 . . . . . 6
983adant3 1016 . . . . 5
10 grpinvadd.p . . . . . 6
114, 10grpcl 15935 . . . . 5
121, 7, 9, 11syl3anc 1228 . . . 4
134, 10grpass 15936 . . . 4
141, 2, 3, 12, 13syl13anc 1230 . . 3
15 eqid 2467 . . . . . . . 8
164, 10, 15, 5grprinv 15969 . . . . . . 7
17163adant2 1015 . . . . . 6
1817oveq1d 6310 . . . . 5
194, 10grpass 15936 . . . . . 6
201, 3, 7, 9, 19syl13anc 1230 . . . . 5
214, 10, 15grplid 15952 . . . . . 6
221, 9, 21syl2anc 661 . . . . 5
2318, 20, 223eqtr3d 2516 . . . 4
2423oveq2d 6311 . . 3
254, 10, 15, 5grprinv 15969 . . . 4