Metamath Proof Explorer


Theorem grpsubid

Description: Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses grpsubid.b B=BaseG
grpsubid.o 0˙=0G
grpsubid.m -˙=-G
Assertion grpsubid GGrpXBX-˙X=0˙

Proof

Step Hyp Ref Expression
1 grpsubid.b B=BaseG
2 grpsubid.o 0˙=0G
3 grpsubid.m -˙=-G
4 eqid +G=+G
5 eqid invgG=invgG
6 1 4 5 3 grpsubval XBXBX-˙X=X+GinvgGX
7 6 anidms XBX-˙X=X+GinvgGX
8 7 adantl GGrpXBX-˙X=X+GinvgGX
9 1 4 2 5 grprinv GGrpXBX+GinvgGX=0˙
10 8 9 eqtrd GGrpXBX-˙X=0˙