Metamath Proof Explorer


Theorem mnd12g

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 + ˙ = + G
mnd4g.1 φ G Mnd
mnd4g.2 φ X B
mnd4g.3 φ Y B
mnd4g.4 φ Z B
mnd12g.5 φ X + ˙ Y = Y + ˙ X
Assertion mnd12g φ X + ˙ Y + ˙ Z = Y + ˙ X + ˙ Z

Proof

Step Hyp Ref Expression
1 mndcl.b B = Base G
2 mndcl.p + ˙ = + G
3 mnd4g.1 φ G Mnd
4 mnd4g.2 φ X B
5 mnd4g.3 φ Y B
6 mnd4g.4 φ Z B
7 mnd12g.5 φ X + ˙ Y = Y + ˙ X
8 7 oveq1d φ X + ˙ Y + ˙ Z = Y + ˙ X + ˙ Z
9 1 2 mndass G Mnd X B Y B Z B X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
10 3 4 5 6 9 syl13anc φ X + ˙ Y + ˙ Z = X + ˙ Y + ˙ Z
11 1 2 mndass G Mnd Y B X B Z B Y + ˙ X + ˙ Z = Y + ˙ X + ˙ Z
12 3 5 4 6 11 syl13anc φ Y + ˙ X + ˙ Z = Y + ˙ X + ˙ Z
13 8 10 12 3eqtr3d φ X + ˙ Y + ˙ Z = Y + ˙ X + ˙ Z