Theorem mnd12g

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$$
	mnd12g.5	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
Assertion	mnd12g	$$⊢\phi \to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Z\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		mnd12g.5	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
8	7	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=\left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Z$$
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(Y\in B\wedge X\in B\wedge Z\in B\right)\right)\to \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Z=Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Z\right)$$
12	3 5 4 6 11	syl13anc	$$⊢\phi \to \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}Z=Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Z\right)$$
13	8 10 12	3eqtr3d	$$⊢\phi \to X\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)=Y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}Z\right)$$