ablnnncan

Description: Cancellation law for group subtraction. ( nnncan analog.) (Contributed by NM, 29-Feb-2008) (Revised by AV, 27-Aug-2021)

	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	ablnnncan	$⊢ φ \to (X \underset{˙}{-} (Y \underset{˙}{-} Z)) \underset{˙}{-} Z = X \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		eqid	$⊢ +_{G} = +_{G}$
8		ablgrp	$⊢ G \in Abel \to G \in Grp$
9	3 8	syl	$⊢ φ \to G \in Grp$
10	1 2	grpsubcl	$⊢ (G \in Grp \land Y \in B \land Z \in B) \to Y \underset{˙}{-} Z \in B$
11	9 5 6 10	syl3anc	$⊢ φ \to Y \underset{˙}{-} Z \in B$
12	1 7 2 3 4 11 6	ablsubsub4	$⊢ φ \to (X \underset{˙}{-} (Y \underset{˙}{-} Z)) \underset{˙}{-} Z = X \underset{˙}{-} ((Y \underset{˙}{-} Z) +_{G} Z)$
13	1 7	ablcom	$⊢ (G \in Abel \land Y \underset{˙}{-} Z \in B \land Z \in B) \to (Y \underset{˙}{-} Z) +_{G} Z = Z +_{G} (Y \underset{˙}{-} Z)$
14	3 11 6 13	syl3anc	$⊢ φ \to (Y \underset{˙}{-} Z) +_{G} Z = Z +_{G} (Y \underset{˙}{-} Z)$
15	1 7 2	ablpncan3	$⊢ (G \in Abel \land (Z \in B \land Y \in B)) \to Z +_{G} (Y \underset{˙}{-} Z) = Y$
16	3 6 5 15	syl12anc	$⊢ φ \to Z +_{G} (Y \underset{˙}{-} Z) = Y$
17	14 16	eqtrd	$⊢ φ \to (Y \underset{˙}{-} Z) +_{G} Z = Y$
18	17	oveq2d	$⊢ φ \to X \underset{˙}{-} ((Y \underset{˙}{-} Z) +_{G} Z) = X \underset{˙}{-} Y$
19	12 18	eqtrd	$⊢ φ \to (X \underset{˙}{-} (Y \underset{˙}{-} Z)) \underset{˙}{-} Z = X \underset{˙}{-} Y$

Metamath Proof Explorer