Metamath Proof Explorer


Theorem ablnncan

Description: Cancellation law for group subtraction. ( nncan analog.) (Contributed by NM, 7-Apr-2015)

Ref Expression
Hypotheses ablnncan.b B=BaseG
ablnncan.m -˙=-G
ablnncan.g φGAbel
ablnncan.x φXB
ablnncan.y φYB
Assertion ablnncan φX-˙X-˙Y=Y

Proof

Step Hyp Ref Expression
1 ablnncan.b B=BaseG
2 ablnncan.m -˙=-G
3 ablnncan.g φGAbel
4 ablnncan.x φXB
5 ablnncan.y φYB
6 eqid +G=+G
7 1 6 2 3 4 4 5 ablsubsub φX-˙X-˙Y=X-˙X+GY
8 ablgrp GAbelGGrp
9 3 8 syl φGGrp
10 eqid 0G=0G
11 1 10 2 grpsubid GGrpXBX-˙X=0G
12 9 4 11 syl2anc φX-˙X=0G
13 12 oveq1d φX-˙X+GY=0G+GY
14 1 6 10 grplid GGrpYB0G+GY=Y
15 9 5 14 syl2anc φ0G+GY=Y
16 7 13 15 3eqtrd φX-˙X-˙Y=Y