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	$⊢ \underset{˙}{+} = +_{G}$
	ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	ablsubadd	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y = Z \leftrightarrow Y \underset{˙}{+} Z = X)$

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

Metamath Proof Explorer