grpnpncan0

Description: Cancellation law for group subtraction ( npncan2 analog). (Contributed by AV, 24-Nov-2019)

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

Step	Hyp	Ref	Expression
1		grpsubadd.b	$⊢ B = {Base}_{G}$
2		grpsubadd.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpsubadd.m	$⊢ \underset{˙}{-} = -_{G}$
4		grpnpncan0.0	$⊢ \underset{˙}{0} = 0_{G}$
5		simpl	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to G \in Grp$
6		simprl	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to X \in B$
7		simprr	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to Y \in B$
8	1 2 3	grpnpncan	$⊢ (G \in Grp \land (X \in B \land Y \in B \land X \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{+} (Y \underset{˙}{-} X) = X \underset{˙}{-} X$
9	5 6 7 6 8	syl13anc	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{+} (Y \underset{˙}{-} X) = X \underset{˙}{-} X$
10	1 4 3	grpsubid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{-} X = \underset{˙}{0}$
11	10	adantrr	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to X \underset{˙}{-} X = \underset{˙}{0}$
12	9 11	eqtrd	$⊢ (G \in Grp \land (X \in B \land Y \in B)) \to (X \underset{˙}{-} Y) \underset{˙}{+} (Y \underset{˙}{-} X) = \underset{˙}{0}$

Metamath Proof Explorer