ablnnncan1

Description: Cancellation law for group subtraction. ( nnncan1 analog.) (Contributed by NM, 7-Apr-2015)

	Ref	Expression
Hypotheses	ablnncan.b	$⊢ B = {Base}_{G}$
	ablnncan.m	$⊢ \underset{˙}{-} = -_{G}$
	ablnncan.g	$⊢ φ \to G \in Abel$
	ablnncan.x	$⊢ φ \to X \in B$
	ablnncan.y	$⊢ φ \to Y \in B$
	ablsub32.z	$⊢ φ \to Z \in B$
Assertion	ablnnncan1	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{-} (X \underset{˙}{-} Z) = Z \underset{˙}{-} Y$

Step	Hyp	Ref	Expression
1		ablnncan.b	$⊢ B = {Base}_{G}$
2		ablnncan.m	$⊢ \underset{˙}{-} = -_{G}$
3		ablnncan.g	$⊢ φ \to G \in Abel$
4		ablnncan.x	$⊢ φ \to X \in B$
5		ablnncan.y	$⊢ φ \to Y \in B$
6		ablsub32.z	$⊢ φ \to Z \in B$
7		ablgrp	$⊢ G \in Abel \to G \in Grp$
8	3 7	syl	$⊢ φ \to G \in Grp$
9	1 2	grpsubcl	$⊢ (G \in Grp \land X \in B \land Z \in B) \to X \underset{˙}{-} Z \in B$
10	8 4 6 9	syl3anc	$⊢ φ \to X \underset{˙}{-} Z \in B$
11	1 2 3 4 5 10	ablsub32	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{-} (X \underset{˙}{-} Z) = (X \underset{˙}{-} (X \underset{˙}{-} Z)) \underset{˙}{-} Y$
12	1 2 3 4 6	ablnncan	$⊢ φ \to X \underset{˙}{-} (X \underset{˙}{-} Z) = Z$
13	12	oveq1d	$⊢ φ \to (X \underset{˙}{-} (X \underset{˙}{-} Z)) \underset{˙}{-} Y = Z \underset{˙}{-} Y$
14	11 13	eqtrd	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{-} (X \underset{˙}{-} Z) = Z \underset{˙}{-} Y$

Metamath Proof Explorer