Metamath Proof Explorer


Theorem grppncan

Description: Cancellation law for subtraction ( pncan analog). (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses grpsubadd.b B=BaseG
grpsubadd.p +˙=+G
grpsubadd.m -˙=-G
Assertion grppncan GGrpXBYBX+˙Y-˙Y=X

Proof

Step Hyp Ref Expression
1 grpsubadd.b B=BaseG
2 grpsubadd.p +˙=+G
3 grpsubadd.m -˙=-G
4 simp1 GGrpXBYBGGrp
5 simp2 GGrpXBYBXB
6 simp3 GGrpXBYBYB
7 1 2 3 grpaddsubass GGrpXBYBYBX+˙Y-˙Y=X+˙Y-˙Y
8 4 5 6 6 7 syl13anc GGrpXBYBX+˙Y-˙Y=X+˙Y-˙Y
9 eqid 0G=0G
10 1 9 3 grpsubid GGrpYBY-˙Y=0G
11 10 oveq2d GGrpYBX+˙Y-˙Y=X+˙0G
12 11 3adant2 GGrpXBYBX+˙Y-˙Y=X+˙0G
13 1 2 9 grprid GGrpXBX+˙0G=X
14 13 3adant3 GGrpXBYBX+˙0G=X
15 8 12 14 3eqtrd GGrpXBYBX+˙Y-˙Y=X