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

Theorem grpoinvid1 21818
 Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
grpinv.1
grpinv.2 GId
grpinv.3
Assertion
Ref Expression
grpoinvid1

Proof of Theorem grpoinvid1
StepHypRef Expression
1 oveq2 6089 . . . 4
3 grpinv.1 . . . . . 6
4 grpinv.2 . . . . . 6 GId
5 grpinv.3 . . . . . 6
63, 4, 5grporinv 21817 . . . . 5
763adant3 977 . . . 4
92, 8eqtr3d 2470 . 2
10 oveq2 6089 . . . 4
123, 4, 5grpolinv 21816 . . . . . . . 8
1312oveq1d 6096 . . . . . . 7
14133adant3 977 . . . . . 6
153, 5grpoinvcl 21814 . . . . . . . . . 10
1615adantrr 698 . . . . . . . . 9
17 simprl 733 . . . . . . . . 9
18 simprr 734 . . . . . . . . 9
1916, 17, 183jca 1134 . . . . . . . 8
203grpoass 21791 . . . . . . . 8
2119, 20syldan 457 . . . . . . 7
22213impb 1149 . . . . . 6
2314, 22eqtr3d 2470 . . . . 5
243, 4grpolid 21807 . . . . . 6
25243adant2 976 . . . . 5
2623, 25eqtr3d 2470 . . . 4