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

Metamath Proof Explorer

Theorem cmnbascntr

Description: The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025)

Ref Expression
Hypotheses cmnbascntr.b ⊢ B = Base G
cmnbascntr.z ⊢ Z = Cntr ⁡ G
Assertion cmnbascntr ⊢ G ∈ CMnd → B = Z

Proof

Step Hyp Ref Expression
1 cmnbascntr.b ⊢ B = Base G
2 cmnbascntr.z ⊢ Z = Cntr ⁡ G
3 eqid ⊢ Cntz ⁡ G = Cntz ⁡ G
4 1 3 cntrval ⊢ Cntz ⁡ G ⁡ B = Cntr ⁡ G
5 ssid ⊢ B ⊆ B
6 eqid ⊢ + G = + G
7 1 6 3 cntzval ⊢ B ⊆ B → Cntz ⁡ G ⁡ B = x ∈ B | ∀ y ∈ B x + G y = y + G x
8 5 7 ax-mp ⊢ Cntz ⁡ G ⁡ B = x ∈ B | ∀ y ∈ B x + G y = y + G x
9 2 4 8 3eqtr2i ⊢ Z = x ∈ B | ∀ y ∈ B x + G y = y + G x
10 1 6 cmncom ⊢ G ∈ CMnd ∧ x ∈ B ∧ y ∈ B → x + G y = y + G x
11 10 3expa ⊢ G ∈ CMnd ∧ x ∈ B ∧ y ∈ B → x + G y = y + G x
12 11 ralrimiva ⊢ G ∈ CMnd ∧ x ∈ B → ∀ y ∈ B x + G y = y + G x
13 12 rabeqcda ⊢ G ∈ CMnd → x ∈ B | ∀ y ∈ B x + G y = y + G x = B
14 9 13 eqtr2id ⊢ G ∈ CMnd → B = Z