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

Theorem grpopnpcan2 21833
 Description: Cancellation law for mixed addition and group division. (pnpcan2 9333 analog.) (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)
Hypotheses
Ref Expression
grpdivf.1
grpdivf.3
Assertion
Ref Expression
grpopnpcan2

Proof of Theorem grpopnpcan2
StepHypRef Expression
1 simpl 444 . . 3
2 grpdivf.1 . . . . 5
32grpocl 21780 . . . 4
52grpocl 21780 . . . 4
7 eqid 2435 . . . 4
8 grpdivf.3 . . . 4
92, 7, 8grpodivval 21823 . . 3
101, 4, 6, 9syl3anc 1184 . 2
112, 7grpoinvop 21821 . . . 4
1312oveq2d 6089 . 2
14 eqid 2435 . . . . . . . . 9 GId GId
152, 14, 7grporinv 21809 . . . . . . . 8 GId
16153adant2 976 . . . . . . 7 GId
1716oveq1d 6088 . . . . . 6 GId
18 simp1 957 . . . . . . 7
19 simp3 959 . . . . . . 7
202, 7grpoinvcl 21806 . . . . . . . 8
21203adant2 976 . . . . . . 7
222, 7grpoinvcl 21806 . . . . . . . 8
23223adant3 977 . . . . . . 7
242grpoass 21783 . . . . . . 7
2518, 19, 21, 23, 24syl13anc 1186 . . . . . 6
262, 14grpolid 21799 . . . . . . . 8 GId
2722, 26syldan 457 . . . . . . 7 GId
28273adant3 977 . . . . . 6 GId
2917, 25, 283eqtr3d 2475 . . . . 5
30293adant3r1 1162 . . . 4
3130oveq2d 6089 . . 3
32 simpr1 963 . . . 4
33 simpr3 965 . . . 4
34203ad2antr3 1124 . . . . 5
35223ad2antr2 1123 . . . . 5
362grpocl 21780 . . . . 5
371, 34, 35, 36syl3anc 1184 . . . 4
382grpoass 21783 . . . 4
391, 32, 33, 37, 38syl13anc 1186 . . 3
402, 7, 8grpodivval 21823 . . . 4