cmn4

Description: Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	ablcom.b	$⊢ B = {Base}_{G}$
	ablcom.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	cmn4	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W)$

Step	Hyp	Ref	Expression
1		ablcom.b	$⊢ B = {Base}_{G}$
2		ablcom.p	$⊢ \underset{˙}{+} = +_{G}$
3		simp1	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to G \in CMnd$
4		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
5	3 4	syl	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to G \in Mnd$
6		simp2l	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to X \in B$
7		simp2r	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \in B$
8		simp3l	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Z \in B$
9		simp3r	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to W \in B$
10	1 2	cmncom	$⊢ (G \in CMnd \land Y \in B \land Z \in B) \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
11	3 7 8 10	syl3anc	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
12	1 2 5 6 7 8 9 11	mnd4g	$⊢ (G \in CMnd \land (X \in B \land Y \in B) \land (Z \in B \land W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W)$

Metamath Proof Explorer