ablsub32

Description: Swap the second and third terms in a double group subtraction. (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	ablsub32	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{-} Z = (X \underset{˙}{-} 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		eqid	$⊢ +_{G} = +_{G}$
8	1 7	ablcom	$⊢ (G \in Abel \land Y \in B \land Z \in B) \to Y +_{G} Z = Z +_{G} Y$
9	3 5 6 8	syl3anc	$⊢ φ \to Y +_{G} Z = Z +_{G} Y$
10	9	oveq2d	$⊢ φ \to X \underset{˙}{-} (Y +_{G} Z) = X \underset{˙}{-} (Z +_{G} Y)$
11	1 7 2 3 4 5 6	ablsubsub4	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{-} Z = X \underset{˙}{-} (Y +_{G} Z)$
12	1 7 2 3 4 6 5	ablsubsub4	$⊢ φ \to (X \underset{˙}{-} Z) \underset{˙}{-} Y = X \underset{˙}{-} (Z +_{G} Y)$
13	10 11 12	3eqtr4d	$⊢ φ \to (X \underset{˙}{-} Y) \underset{˙}{-} Z = (X \underset{˙}{-} Z) \underset{˙}{-} Y$

Metamath Proof Explorer