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

Theorem grpoinvid2 25359
 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
grpoinvid2

Proof of Theorem grpoinvid2
StepHypRef Expression
1 oveq1 6303 . . . 4
3 grpinv.1 . . . . . 6
4 grpinv.2 . . . . . 6 GId
5 grpinv.3 . . . . . 6
63, 4, 5grpolinv 25356 . . . . 5
763adant3 1016 . . . 4
92, 8eqtr3d 2500 . 2
103, 5grpoinvcl 25354 . . . . . . 7
113, 4grpolid 25347 . . . . . . 7
1210, 11syldan 470 . . . . . 6
13123adant3 1016 . . . . 5
1413eqcomd 2465 . . . 4
16 oveq1 6303 . . . 4
18 simprr 757 . . . . . . . 8
19 simprl 756 . . . . . . . 8
2010adantrr 716 . . . . . . . 8
2118, 19, 203jca 1176 . . . . . . 7
223grpoass 25331 . . . . . . 7
2321, 22syldan 470 . . . . . 6
24233impb 1192 . . . . 5
253, 4, 5grporinv 25357 . . . . . . 7
2625oveq2d 6312 . . . . . 6
27263adant3 1016 . . . . 5
283, 4grporid 25348 . . . . . 6
29283adant2 1015 . . . . 5
3024, 27, 293eqtrd 2502 . . . 4