Metamath Proof Explorer

Theorem abladdsub

Description: Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014)

		Ref	Expression
	Hypotheses	ablsubadd.b	$⊢ B = {Base}_{G}$
		ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
		ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
	Assertion	abladdsub	$⊢ (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$

Proof

Step	Hyp	Ref	Expression
1		ablsubadd.b	$⊢ B = {Base}_{G}$
2		ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4	1 2	ablcom	$⊢ (G \in Abel \land X \in B \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
5	4	3adant3r3	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
6	5	oveq1d	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} Z = (Y \underset{˙}{+} X) \underset{˙}{-} Z$
7		ablgrp	$⊢ G \in Abel \to G \in Grp$
8	7	adantr	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to G \in Grp$
9		simpr2	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
10		simpr1	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
11		simpr3	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
12	1 2 3	grpaddsubass	$⊢ (G \in Grp \land (Y \in B \land X \in B \land Z \in B)) \to (Y \underset{˙}{+} X) \underset{˙}{-} Z = Y \underset{˙}{+} (X \underset{˙}{-} Z)$
13	8 9 10 11 12	syl13anc	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{+} X) \underset{˙}{-} Z = Y \underset{˙}{+} (X \underset{˙}{-} Z)$
14		simpl	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to G \in Abel$
15	1 3	grpsubcl	$⊢ (G \in Grp \land X \in B \land Z \in B) \to X \underset{˙}{-} Z \in B$
16	8 10 11 15	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{-} Z \in B$
17	1 2	ablcom	$⊢ (G \in Abel \land Y \in B \land X \underset{˙}{-} Z \in B) \to Y \underset{˙}{+} (X \underset{˙}{-} Z) = (X \underset{˙}{-} Z) \underset{˙}{+} Y$
18	14 9 16 17	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{+} (X \underset{˙}{-} Z) = (X \underset{˙}{-} Z) \underset{˙}{+} Y$
19	6 13 18	3eqtrd	$⊢ (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$