Description: Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grpsubid.b | |
|
grpsubid.o | |
||
grpsubid.m | |
||
Assertion | grpsubid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpsubid.b | |
|
2 | grpsubid.o | |
|
3 | grpsubid.m | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 1 4 5 3 | grpsubval | |
7 | 6 | anidms | |
8 | 7 | adantl | |
9 | 1 4 2 5 | grprinv | |
10 | 8 9 | eqtrd | |