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

Metamath Proof Explorer

Theorem iscmn

Description: The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses iscmn.b ⊢ B = Base G
iscmn.p ⊢ + ˙ = + G
Assertion iscmn ⊢ G ∈ CMnd ↔ G ∈ Mnd ∧ ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x

Proof

Step Hyp Ref Expression
1 iscmn.b ⊢ B = Base G
2 iscmn.p ⊢ + ˙ = + G
3 fveq2 ⊢ g = G → Base g = Base G
4 3 1 eqtr4di ⊢ g = G → Base g = B
5 raleq ⊢ Base g = B → ∀ y ∈ Base g x + g y = y + g x ↔ ∀ y ∈ B x + g y = y + g x
6 5 raleqbi1dv ⊢ Base g = B → ∀ x ∈ Base g ∀ y ∈ Base g x + g y = y + g x ↔ ∀ x ∈ B ∀ y ∈ B x + g y = y + g x
7 4 6 syl ⊢ g = G → ∀ x ∈ Base g ∀ y ∈ Base g x + g y = y + g x ↔ ∀ x ∈ B ∀ y ∈ B x + g y = y + g x
8 fveq2 ⊢ g = G → + g = + G
9 8 2 eqtr4di ⊢ g = G → + g = + ˙
10 9 oveqd ⊢ g = G → x + g y = x + ˙ y
11 9 oveqd ⊢ g = G → y + g x = y + ˙ x
12 10 11 eqeq12d ⊢ g = G → x + g y = y + g x ↔ x + ˙ y = y + ˙ x
13 12 2ralbidv ⊢ g = G → ∀ x ∈ B ∀ y ∈ B x + g y = y + g x ↔ ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x
14 7 13 bitrd ⊢ g = G → ∀ x ∈ Base g ∀ y ∈ Base g x + g y = y + g x ↔ ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x
15 df-cmn ⊢ CMnd = g ∈ Mnd | ∀ x ∈ Base g ∀ y ∈ Base g x + g y = y + g x
16 14 15 elrab2 ⊢ G ∈ CMnd ↔ G ∈ Mnd ∧ ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x