This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mnd4g

Description: Commutative/associative law for commutative 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$
		mnd4g.5	$⊢ φ \to W \in B$
		mnd4g.6	$⊢ φ \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
	Assertion	mnd4g	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W)$

Proof

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		mnd4g.5	$⊢ φ \to W \in B$
8		mnd4g.6	$⊢ φ \to Y \underset{˙}{+} Z = Z \underset{˙}{+} Y$
9	1 2 3 5 6 7 8	mnd12g	$⊢ φ \to Y \underset{˙}{+} (Z \underset{˙}{+} W) = Z \underset{˙}{+} (Y \underset{˙}{+} W)$
10	9	oveq2d	$⊢ φ \to X \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W)) = X \underset{˙}{+} (Z \underset{˙}{+} (Y \underset{˙}{+} W))$
11	1 2	mndcl	$⊢ (G \in Mnd \land Z \in B \land W \in B) \to Z \underset{˙}{+} W \in B$
12	3 6 7 11	syl3anc	$⊢ φ \to Z \underset{˙}{+} W \in B$
13	1 2	mndass	$⊢ (G \in Mnd \land (X \in B \land Y \in B \land Z \underset{˙}{+} W \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = X \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W))$
14	3 4 5 12 13	syl13anc	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = X \underset{˙}{+} (Y \underset{˙}{+} (Z \underset{˙}{+} W))$
15	1 2	mndcl	$⊢ (G \in Mnd \land Y \in B \land W \in B) \to Y \underset{˙}{+} W \in B$
16	3 5 7 15	syl3anc	$⊢ φ \to Y \underset{˙}{+} W \in B$
17	1 2	mndass	$⊢ (G \in Mnd \land (X \in B \land Z \in B \land Y \underset{˙}{+} W \in B)) \to (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W) = X \underset{˙}{+} (Z \underset{˙}{+} (Y \underset{˙}{+} W))$
18	3 4 6 16 17	syl13anc	$⊢ φ \to (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W) = X \underset{˙}{+} (Z \underset{˙}{+} (Y \underset{˙}{+} W))$
19	10 14 18	3eqtr4d	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{+} (Z \underset{˙}{+} W) = (X \underset{˙}{+} Z) \underset{˙}{+} (Y \underset{˙}{+} W)$