Theorem abl32

Description: Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015) (Revised by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	ablcom.b	$$⊢B={\mathrm{Base}}_G$$
	ablcom.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	abl32.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	abl32.x	$$⊢\phi \to X\in B$$
	abl32.y	$$⊢\phi \to Y\in B$$
	abl32.z	$$⊢\phi \to Z\in B$$
Assertion	abl32	$$⊢\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		ablcom.b	$$⊢B={\mathrm{Base}}_G$$
2		ablcom.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		abl32.g	$$⊢\phi \to G\in \mathrm{Abel}$$
4		abl32.x	$$⊢\phi \to X\in B$$
5		abl32.y	$$⊢\phi \to Y\in B$$
6		abl32.z	$$⊢\phi \to Z\in B$$
7		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
8	3 7	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
9	1 2	cmn32	$$⊢\left(G\in \mathrm{CMnd}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}Y$$
10	8 4 5 6 9	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}Y$$