ablpncan2

Description: Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014)

	Ref	Expression
Hypotheses	ablsubadd.b	$⊢ B = {Base}_{G}$
	ablsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
	ablsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	ablpncan2	$⊢ (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		simp1	$⊢ (G \in Abel \land X \in B \land Y \in B) \to G \in Abel$
5		simp2	$⊢ (G \in Abel \land X \in B \land Y \in B) \to X \in B$
6		simp3	$⊢ (G \in Abel \land X \in B \land Y \in B) \to Y \in B$
7	1 2 3	abladdsub	$⊢ (G \in Abel \land (X \in B \land Y \in B \land X \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{-} X = (X \underset{˙}{-} X) \underset{˙}{+} Y$
8	4 5 6 5 7	syl13anc	$⊢ (G \in Abel \land X \in B \land Y \in B) \to (X \underset{˙}{+} Y) \underset{˙}{-} X = (X \underset{˙}{-} X) \underset{˙}{+} Y$
9		ablgrp	$⊢ G \in Abel \to G \in Grp$
10	4 9	syl	$⊢ (G \in Abel \land X \in B \land Y \in B) \to G \in Grp$
11		eqid	$⊢ 0_{G} = 0_{G}$
12	1 11 3	grpsubid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{-} X = 0_{G}$
13	10 5 12	syl2anc	$⊢ (G \in Abel \land X \in B \land Y \in B) \to X \underset{˙}{-} X = 0_{G}$
14	13	oveq1d	$⊢ (G \in Abel \land X \in B \land Y \in B) \to (X \underset{˙}{-} X) \underset{˙}{+} Y = 0_{G} \underset{˙}{+} Y$
15	1 2 11	grplid	$⊢ (G \in Grp \land Y \in B) \to 0_{G} \underset{˙}{+} Y = Y$
16	10 6 15	syl2anc	$⊢ (G \in Abel \land X \in B \land Y \in B) \to 0_{G} \underset{˙}{+} Y = Y$
17	8 14 16	3eqtrd	$⊢ (G \in Abel \land X \in B \land Y \in B) \to (X \underset{˙}{+} Y) \underset{˙}{-} X = Y$

Metamath Proof Explorer