Description: Subtraction expressed as addition of the difference of the identity element and the subtrahend. (Contributed by AV, 9-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grpsubid.b | |
|
grpsubid.o | |
||
grpsubid.m | |
||
grpsubadd0sub.p | |
||
Assertion | grpsubadd0sub | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpsubid.b | |
|
2 | grpsubid.o | |
|
3 | grpsubid.m | |
|
4 | grpsubadd0sub.p | |
|
5 | eqid | |
|
6 | 1 4 5 3 | grpsubval | |
7 | 6 | 3adant1 | |
8 | 1 3 5 2 | grpinvval2 | |
9 | 8 | 3adant2 | |
10 | 9 | oveq2d | |
11 | 7 10 | eqtrd | |