ablpncan3

Description: A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015)

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

Step	Hyp	Ref	Expression
1		ablsubadd.b	$⊢ B = {Base}_{G}$
2		ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		simpl	$⊢ (G \in Abel \land (X \in B \land Y \in B)) \to G \in Abel$
5		simprl	$⊢ (G \in Abel \land (X \in B \land Y \in B)) \to X \in B$
6		ablgrp	$⊢ G \in Abel \to G \in Grp$
7	6	adantr	$⊢ (G \in Abel \land (X \in B \land Y \in B)) \to G \in Grp$
8		simprr	$⊢ (G \in Abel \land (X \in B \land Y \in B)) \to Y \in B$
9	1 3	grpsubcl	$⊢ (G \in Grp \land Y \in B \land X \in B) \to Y \underset{˙}{-} X \in B$
10	7 8 5 9	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B)) \to Y \underset{˙}{-} X \in B$
11	1 2	ablcom	$⊢ (G \in Abel \land X \in B \land Y \underset{˙}{-} X \in B) \to X \underset{˙}{+} (Y \underset{˙}{-} X) = (Y \underset{˙}{-} X) \underset{˙}{+} X$
12	4 5 10 11	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B)) \to X \underset{˙}{+} (Y \underset{˙}{-} X) = (Y \underset{˙}{-} X) \underset{˙}{+} X$
13	1 2 3	grpnpcan	$⊢ (G \in Grp \land Y \in B \land X \in B) \to (Y \underset{˙}{-} X) \underset{˙}{+} X = Y$
14	7 8 5 13	syl3anc	$⊢ (G \in Abel \land (X \in B \land Y \in B)) \to (Y \underset{˙}{-} X) \underset{˙}{+} X = Y$
15	12 14	eqtrd	$⊢ (G \in Abel \land (X \in B \land Y \in B)) \to X \underset{˙}{+} (Y \underset{˙}{-} X) = Y$

Metamath Proof Explorer