Metamath Proof Explorer

Theorem cmn12

Description: Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015) (Revised by Mario Carneiro, 21-Apr-2016)

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

Proof

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 X \in B \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
9	8	3adant3r3	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
10	1 2 4 5 6 7 9	mnd12g	$⊢ (G \in CMnd \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) = Y \underset{˙}{+} (X \underset{˙}{+} Z)$