Theorem 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={\mathrm{Base}}_G$$
	ablnncan.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	ablnncan.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	ablnncan.x	$$⊢\phi \to X\in B$$
	ablnncan.y	$$⊢\phi \to Y\in B$$
	ablsub32.z	$$⊢\phi \to Z\in B$$
Assertion	ablsub32	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z=\left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y$$

Proof

Step	Hyp	Ref	Expression
1		ablnncan.b	$$⊢B={\mathrm{Base}}_G$$
2		ablnncan.m	$$⊢\underset{\dot{}}{-}={-}_G$$
3		ablnncan.g	$$⊢\phi \to G\in \mathrm{Abel}$$
4		ablnncan.x	$$⊢\phi \to X\in B$$
5		ablnncan.y	$$⊢\phi \to Y\in B$$
6		ablsub32.z	$$⊢\phi \to Z\in B$$
7		eqid	$$⊢{+}_G={+}_G$$
8	1 7	ablcom	$$⊢\left(G\in \mathrm{Abel}\wedge Y\in B\wedge Z\in B\right)\to Y{+}_{G}Z=Z{+}_{G}Y$$
9	3 5 6 8	syl3anc	$$⊢\phi \to Y{+}_{G}Z=Z{+}_{G}Y$$
10	9	oveq2d	$$⊢\phi \to X\underset{\dot{}}{-}\left(Y{+}_{G}Z\right)=X\underset{\dot{}}{-}\left(Z{+}_{G}Y\right)$$
11	1 7 2 3 4 5 6	ablsubsub4	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}\left(Y{+}_{G}Z\right)$$
12	1 7 2 3 4 6 5	ablsubsub4	$$⊢\phi \to \left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y=X\underset{\dot{}}{-}\left(Z{+}_{G}Y\right)$$
13	10 11 12	3eqtr4d	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z=\left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y$$