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

Theorem grpinvid2 14856
 Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.)
Hypotheses
Ref Expression
grpinv.b
grpinv.p
grpinv.u
grpinv.n
Assertion
Ref Expression
grpinvid2

Proof of Theorem grpinvid2
StepHypRef Expression
1 oveq1 6090 . . . 4
3 grpinv.b . . . . . 6
4 grpinv.p . . . . . 6
5 grpinv.u . . . . . 6
6 grpinv.n . . . . . 6
73, 4, 5, 6grplinv 14853 . . . . 5
873adant3 978 . . . 4
102, 9eqtr3d 2472 . 2
113, 6grpinvcl 14852 . . . . . . 7
123, 4, 5grplid 14837 . . . . . . 7
1311, 12syldan 458 . . . . . 6
14133adant3 978 . . . . 5
1514eqcomd 2443 . . . 4
17 oveq1 6090 . . . 4
19 simprr 735 . . . . . . . 8
20 simprl 734 . . . . . . . 8
2111adantrr 699 . . . . . . . 8
2219, 20, 213jca 1135 . . . . . . 7
233, 4grpass 14821 . . . . . . 7
2422, 23syldan 458 . . . . . 6
25243impb 1150 . . . . 5
263, 4, 5, 6grprinv 14854 . . . . . . 7
2726oveq2d 6099 . . . . . 6
28273adant3 978 . . . . 5
293, 4, 5grprid 14838 . . . . . 6
30293adant2 977 . . . . 5
3125, 28, 303eqtrd 2474 . . . 4