Theorem cmn4d

Description: Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	cmn4d.1	$$⊢B={\mathrm{Base}}_G$$
	cmn4d.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	cmn4d.3	$$⊢\phi \to G\in \mathrm{CMnd}$$
	cmn4d.4	$$⊢\phi \to X\in B$$
	cmn4d.5	$$⊢\phi \to Y\in B$$
	cmn4d.6	$$⊢\phi \to Z\in B$$
	cmn4d.7	$$⊢\phi \to W\in B$$
Assertion	cmn4d	$$⊢\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		cmn4d.1	$$⊢B={\mathrm{Base}}_G$$
2		cmn4d.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		cmn4d.3	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		cmn4d.4	$$⊢\phi \to X\in B$$
5		cmn4d.5	$$⊢\phi \to Y\in B$$
6		cmn4d.6	$$⊢\phi \to Z\in B$$
7		cmn4d.7	$$⊢\phi \to W\in B$$
8	1 2	cmn4	$$⊢\left(G\in \mathrm{CMnd}\wedge \left(X\in B\wedge Y\in B\right)\wedge \left(Z\in B\wedge W\in B\right)\right)\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)$$
9	3 4 5 6 7 8	syl122anc	$$⊢\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)$$