Theorem ablsubadd

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

	Ref	Expression
Hypotheses	ablsubadd.b	$$⊢B={\mathrm{Base}}_G$$
	ablsubadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	ablsubadd.m	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	ablsubadd	$$⊢\left(G\in \mathrm{Abel}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{-}Y=Z\leftrightarrow Y\underset{\dot{}}{+}Z=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	$$⊢B={\mathrm{Base}}_G$$
2		ablsubadd.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		ablsubadd.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
5	1 2 3	grpsubadd	$$⊢\left(G\in \mathrm{Grp}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{-}Y=Z\leftrightarrow Z\underset{\dot{}}{+}Y=X\right)$$
6	4 5	sylan	$$⊢\left(G\in \mathrm{Abel}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{-}Y=Z\leftrightarrow Z\underset{\dot{}}{+}Y=X\right)$$
7	1 2	ablcom	$$⊢\left(G\in \mathrm{Abel}\wedge Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
8	7	3adant3r1	$$⊢\left(G\in \mathrm{Abel}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
9	8	eqeq1d	$$⊢\left(G\in \mathrm{Abel}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(Y\underset{\dot{}}{+}Z=X\leftrightarrow Z\underset{\dot{}}{+}Y=X\right)$$
10	6 9	bitr4d	$$⊢\left(G\in \mathrm{Abel}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{-}Y=Z\leftrightarrow Y\underset{\dot{}}{+}Z=X\right)$$