Metamath Proof Explorer


Theorem grpsubadd0sub

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 B=BaseG
grpsubid.o 0˙=0G
grpsubid.m -˙=-G
grpsubadd0sub.p +˙=+G
Assertion grpsubadd0sub GGrpXBYBX-˙Y=X+˙0˙-˙Y

Proof

Step Hyp Ref Expression
1 grpsubid.b B=BaseG
2 grpsubid.o 0˙=0G
3 grpsubid.m -˙=-G
4 grpsubadd0sub.p +˙=+G
5 eqid invgG=invgG
6 1 4 5 3 grpsubval XBYBX-˙Y=X+˙invgGY
7 6 3adant1 GGrpXBYBX-˙Y=X+˙invgGY
8 1 3 5 2 grpinvval2 GGrpYBinvgGY=0˙-˙Y
9 8 3adant2 GGrpXBYBinvgGY=0˙-˙Y
10 9 oveq2d GGrpXBYBX+˙invgGY=X+˙0˙-˙Y
11 7 10 eqtrd GGrpXBYBX-˙Y=X+˙0˙-˙Y