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

Metamath Proof Explorer

Theorem iscmnd

Description: Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses iscmnd.b ⊢ φ → B = Base G
iscmnd.p ⊢ φ → + ˙ = + G
iscmnd.g ⊢ φ → G ∈ Mnd
iscmnd.c ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + ˙ y = y + ˙ x
Assertion iscmnd ⊢ φ → G ∈ CMnd

Proof

Step Hyp Ref Expression
1 iscmnd.b ⊢ φ → B = Base G
2 iscmnd.p ⊢ φ → + ˙ = + G
3 iscmnd.g ⊢ φ → G ∈ Mnd
4 iscmnd.c ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + ˙ y = y + ˙ x
5 4 3expib ⊢ φ → x ∈ B ∧ y ∈ B → x + ˙ y = y + ˙ x
6 5 ralrimivv ⊢ φ → ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x
7 2 oveqd ⊢ φ → x + ˙ y = x + G y
8 2 oveqd ⊢ φ → y + ˙ x = y + G x
9 7 8 eqeq12d ⊢ φ → x + ˙ y = y + ˙ x ↔ x + G y = y + G x
10 1 9 raleqbidv ⊢ φ → ∀ y ∈ B x + ˙ y = y + ˙ x ↔ ∀ y ∈ Base G x + G y = y + G x
11 1 10 raleqbidv ⊢ φ → ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x ↔ ∀ x ∈ Base G ∀ y ∈ Base G x + G y = y + G x
12 11 anbi2d ⊢ φ → G ∈ Mnd ∧ ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x ↔ G ∈ Mnd ∧ ∀ x ∈ Base G ∀ y ∈ Base G x + G y = y + G x
13 3 6 12 mpbi2and ⊢ φ → G ∈ Mnd ∧ ∀ x ∈ Base G ∀ y ∈ Base G x + G y = y + G x
14 eqid ⊢ Base G = Base G
15 eqid ⊢ + G = + G
16 14 15 iscmn ⊢ G ∈ CMnd ↔ G ∈ Mnd ∧ ∀ x ∈ Base G ∀ y ∈ Base G x + G y = y + G x
17 13 16 sylibr ⊢ φ → G ∈ CMnd