Theorem mnd32g

Description: Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	mndcl.b	$$⊢B={\mathrm{Base}}_G$$
	mndcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mnd4g.1	$$⊢\phi \to G\in \mathrm{Mnd}$$
	mnd4g.2	$$⊢\phi \to X\in B$$
	mnd4g.3	$$⊢\phi \to Y\in B$$
	mnd4g.4	$$⊢\phi \to Z\in B$$
	mnd32g.5	$$⊢\phi \to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
Assertion	mnd32g	$$⊢\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		mndcl.b	$$⊢B={\mathrm{Base}}_G$$
2		mndcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mnd4g.1	$$⊢\phi \to G\in \mathrm{Mnd}$$
4		mnd4g.2	$$⊢\phi \to X\in B$$
5		mnd4g.3	$$⊢\phi \to Y\in B$$
6		mnd4g.4	$$⊢\phi \to Z\in B$$
7		mnd32g.5	$$⊢\phi \to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
8	7	oveq2d	$$⊢\phi \to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)$$
9	1 2	mndass	$$⊢\left(G\in \mathrm{Mnd}\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=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$
10	3 4 5 6 9	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$
11	1 2	mndass	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(X\in B\wedge Z\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)$$
12	3 4 6 5 11	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}Y\right)$$
13	8 10 12	3eqtr4d	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}Y$$