mnd32g

Description: Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	mndcl.b	$⊢ B = {Base}_{G}$
	mndcl.p	$⊢ \underset{˙}{+} = +_{G}$
	mnd4g.1	$⊢ φ \to G \in Mnd$
	mnd4g.2	$⊢ φ \to X \in B$
	mnd4g.3	$⊢ φ \to Y \in B$
	mnd4g.4	$⊢ φ \to Z \in B$
	mnd32g.5	$⊢ φ \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
Assertion	mnd32g	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = (X \underset{˙}{+} Z) \underset{˙}{+} Y$

Step	Hyp	Ref	Expression
1		mndcl.b	$⊢ B = {Base}_{G}$
2		mndcl.p	$⊢ \underset{˙}{+} = +_{G}$
3		mnd4g.1	$⊢ φ \to G \in Mnd$
4		mnd4g.2	$⊢ φ \to X \in B$
5		mnd4g.3	$⊢ φ \to Y \in B$
6		mnd4g.4	$⊢ φ \to Z \in B$
7		mnd32g.5	$⊢ φ \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
8	7	oveq2d	$⊢ φ \to X \underset{˙}{+} (Y \underset{˙}{+} Z) = X \underset{˙}{+} (Z \underset{˙}{+} Y)$
9	1 2	mndass	$⊢ (G \in Mnd \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = X \underset{˙}{+} (Y \underset{˙}{+} Z)$
10	3 4 5 6 9	syl13anc	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = X \underset{˙}{+} (Y \underset{˙}{+} Z)$
11	1 2	mndass	$⊢ (G \in Mnd \land (X \in B \land Z \in B \land Y \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{+} Y = X \underset{˙}{+} (Z \underset{˙}{+} Y)$
12	3 4 6 5 11	syl13anc	$⊢ φ \to (X \underset{˙}{+} Z) \underset{˙}{+} Y = X \underset{˙}{+} (Z \underset{˙}{+} Y)$
13	8 10 12	3eqtr4d	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} Z = (X \underset{˙}{+} Z) \underset{˙}{+} Y$

Metamath Proof Explorer