Metamath Proof Explorer


Theorem ablsubadd

Description: Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses ablsubadd.b B = Base G
ablsubadd.p + ˙ = + G
ablsubadd.m - ˙ = - G
Assertion ablsubadd G Abel X B Y B Z B X - ˙ Y = Z Y + ˙ Z = X

Proof

Step Hyp Ref Expression
1 ablsubadd.b B = Base G
2 ablsubadd.p + ˙ = + G
3 ablsubadd.m - ˙ = - G
4 ablgrp G Abel G Grp
5 1 2 3 grpsubadd G Grp X B Y B Z B X - ˙ Y = Z Z + ˙ Y = X
6 4 5 sylan G Abel X B Y B Z B X - ˙ Y = Z Z + ˙ Y = X
7 1 2 ablcom G Abel Y B Z B Y + ˙ Z = Z + ˙ Y
8 7 3adant3r1 G Abel X B Y B Z B Y + ˙ Z = Z + ˙ Y
9 8 eqeq1d G Abel X B Y B Z B Y + ˙ Z = X Z + ˙ Y = X
10 6 9 bitr4d G Abel X B Y B Z B X - ˙ Y = Z Y + ˙ Z = X