cmn32

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	cmn32	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = (X \underset{˙}{+} Z) \underset{˙}{+} Y$

Step	Hyp	Ref	Expression
1		ablcom.b	$⊢ B = {Base}_{G}$
2		ablcom.p	$⊢ \underset{˙}{+} = +_{G}$
3		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
4	3	adantr	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to G \in Mnd$
5		simpr1	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
6		simpr2	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
7		simpr3	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
8	1 2	cmncom	$⊢ (G \in CMnd \land Y \in B \land Z \in B) \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
9	8	3adant3r1	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
10	1 2 4 5 6 7 9	mnd32g	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = (X \underset{˙}{+} Z) \underset{˙}{+} Y$

Metamath Proof Explorer