ablsubadd23

Description: Commutative/associative law for addition and subtraction in abelian groups. ( subadd23d analog.) (Contributed by AV, 2-Mar-2025)

	Ref	Expression
Hypotheses	ablsubadd.b	$⊢ B = {Base}_{G}$
	ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
	ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	ablsubadd23	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{+} Z = X \underset{˙}{+} (Z \underset{˙}{-} Y)$

Step	Hyp	Ref	Expression
1		ablsubadd.b	$⊢ B = {Base}_{G}$
2		ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		3ancomb	$⊢ (X \in B \land Y \in B \land Z \in B) \leftrightarrow (X \in B \land Z \in B \land Y \in B)$
5	4	biimpi	$⊢ (X \in B \land Y \in B \land Z \in B) \to (X \in B \land Z \in B \land Y \in B)$
6	1 2 3	abladdsub	$⊢ (G \in Abel \land (X \in B \land Z \in B \land Y \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{-} Y = (X \underset{˙}{-} Y) \underset{˙}{+} Z$
7	5 6	sylan2	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{-} Y = (X \underset{˙}{-} Y) \underset{˙}{+} Z$
8		ablgrp	$⊢ G \in Abel \to G \in Grp$
9	1 2 3	grpaddsubass	$⊢ (G \in Grp \land (X \in B \land Z \in B \land Y \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{-} Y = X \underset{˙}{+} (Z \underset{˙}{-} Y)$
10	8 5 9	syl2an	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{-} Y = X \underset{˙}{+} (Z \underset{˙}{-} Y)$
11	7 10	eqtr3d	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{+} Z = X \underset{˙}{+} (Z \underset{˙}{-} Y)$

Metamath Proof Explorer