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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mndcl.p	⊢ + = ( +g ‘ 𝐺 )
	mnd4g.1	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	mnd4g.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	mnd4g.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	mnd4g.4	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	mnd4g.5	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	mnd4g.6	⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) = ( 𝑍 + 𝑌 ) )
Assertion	mnd4g	⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( 𝑍 + 𝑊 ) ) = ( ( 𝑋 + 𝑍 ) + ( 𝑌 + 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mndcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mndcl.p	⊢ + = ( +g ‘ 𝐺 )
3		mnd4g.1	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
4		mnd4g.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		mnd4g.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		mnd4g.4	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7		mnd4g.5	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
8		mnd4g.6	⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) = ( 𝑍 + 𝑌 ) )
9	1 2 3 5 6 7 8	mnd12g	⊢ ( 𝜑 → ( 𝑌 + ( 𝑍 + 𝑊 ) ) = ( 𝑍 + ( 𝑌 + 𝑊 ) ) )
10	9	oveq2d	⊢ ( 𝜑 → ( 𝑋 + ( 𝑌 + ( 𝑍 + 𝑊 ) ) ) = ( 𝑋 + ( 𝑍 + ( 𝑌 + 𝑊 ) ) ) )
11	1 2	mndcl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
12	3 6 7 11	syl3anc	⊢ ( 𝜑 → ( 𝑍 + 𝑊 ) ∈ 𝐵 )
13	1 2	mndass	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + ( 𝑍 + 𝑊 ) ) = ( 𝑋 + ( 𝑌 + ( 𝑍 + 𝑊 ) ) ) )
14	3 4 5 12 13	syl13anc	⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( 𝑍 + 𝑊 ) ) = ( 𝑋 + ( 𝑌 + ( 𝑍 + 𝑊 ) ) ) )
15	1 2	mndcl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 + 𝑊 ) ∈ 𝐵 )
16	3 5 7 15	syl3anc	⊢ ( 𝜑 → ( 𝑌 + 𝑊 ) ∈ 𝐵 )
17	1 2	mndass	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( 𝑌 + 𝑊 ) ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) + ( 𝑌 + 𝑊 ) ) = ( 𝑋 + ( 𝑍 + ( 𝑌 + 𝑊 ) ) ) )
18	3 4 6 16 17	syl13anc	⊢ ( 𝜑 → ( ( 𝑋 + 𝑍 ) + ( 𝑌 + 𝑊 ) ) = ( 𝑋 + ( 𝑍 + ( 𝑌 + 𝑊 ) ) ) )
19	10 14 18	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( 𝑍 + 𝑊 ) ) = ( ( 𝑋 + 𝑍 ) + ( 𝑌 + 𝑊 ) ) )