Theorem mnd4g

Description: Commutative/associative law for commutative 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$$
	mnd4g.5	$$⊢\phi \to W\in B$$
	mnd4g.6	$$⊢\phi \to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
Assertion	mnd4g	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}W\right)=\left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}W\right)$$

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		mnd4g.5	$$⊢\phi \to W\in B$$
8		mnd4g.6	$$⊢\phi \to Y\underset{\dot{}}{+}Z=Z\underset{\dot{}}{+}Y$$
9	1 2 3 5 6 7 8	mnd12g	$$⊢\phi \to Y\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}W\right)=Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}W\right)$$
10	9	oveq2d	$$⊢\phi \to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}W\right)\right)=X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}W\right)\right)$$
11	1 2	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge Z\in B\wedge W\in B\right)\to Z\underset{\dot{}}{+}W\in B$$
12	3 6 7 11	syl3anc	$$⊢\phi \to Z\underset{\dot{}}{+}W\in B$$
13	1 2	mndass	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(X\in B\wedge Y\in B\wedge Z\underset{\dot{}}{+}W\in B\right)\right)\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}W\right)=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}W\right)\right)$$
14	3 4 5 12 13	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}W\right)=X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}W\right)\right)$$
15	1 2	mndcl	$$⊢\left(G\in \mathrm{Mnd}\wedge Y\in B\wedge W\in B\right)\to Y\underset{\dot{}}{+}W\in B$$
16	3 5 7 15	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}W\in B$$
17	1 2	mndass	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(X\in B\wedge Z\in B\wedge Y\underset{\dot{}}{+}W\in B\right)\right)\to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}W\right)=X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}W\right)\right)$$
18	3 4 6 16 17	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}W\right)=X\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}W\right)\right)$$
19	10 14 18	3eqtr4d	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}\left(Z\underset{\dot{}}{+}W\right)=\left(X\underset{\dot{}}{+}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}W\right)$$