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

Theorem grpinvid1 15947
 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
grpinvid1

Proof of Theorem grpinvid1
StepHypRef Expression
1 oveq2 6302 . . . 4
3 grpinv.b . . . . . 6
4 grpinv.p . . . . . 6
5 grpinv.u . . . . . 6
6 grpinv.n . . . . . 6
73, 4, 5, 6grprinv 15946 . . . . 5
873adant3 1016 . . . 4
102, 9eqtr3d 2510 . 2
11 oveq2 6302 . . . 4
133, 4, 5, 6grplinv 15945 . . . . . . . 8
1413oveq1d 6309 . . . . . . 7
15143adant3 1016 . . . . . 6
163, 6grpinvcl 15944 . . . . . . . . . 10
1716adantrr 716 . . . . . . . . 9
18 simprl 755 . . . . . . . . 9
19 simprr 756 . . . . . . . . 9
2017, 18, 193jca 1176 . . . . . . . 8
213, 4grpass 15913 . . . . . . . 8
2220, 21syldan 470 . . . . . . 7
23223impb 1192 . . . . . 6
2415, 23eqtr3d 2510 . . . . 5
253, 4, 5grplid 15929 . . . . . 6
26253adant2 1015 . . . . 5
2724, 26eqtr3d 2510 . . . 4