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={\mathrm{Base}}_G$$
	cmnbascntr.z	$$⊢Z=\mathrm{Cntr}\left(G\right)$$
Assertion	cmnbascntr	$$⊢G\in \mathrm{CMnd}\to B=Z$$

Proof

Step	Hyp	Ref	Expression
1		cmnbascntr.b	$$⊢B={\mathrm{Base}}_G$$
2		cmnbascntr.z	$$⊢Z=\mathrm{Cntr}\left(G\right)$$
3		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
4	1 3	cntrval	$$⊢\mathrm{Cntz}\left(G\right)\left(B\right)=\mathrm{Cntr}\left(G\right)$$
5		ssid	$$⊢B\subseteq B$$
6		eqid	$$⊢{+}_G={+}_G$$
7	1 6 3	cntzval	$$⊢B\subseteq B\to \mathrm{Cntz}\left(G\right)\left(B\right)=\left\{x\in B|\forall y\in Bx{+}_{G}y=y{+}_{G}x\right\}$$
8	5 7	ax-mp	$$⊢\mathrm{Cntz}\left(G\right)\left(B\right)=\left\{x\in B|\forall y\in Bx{+}_{G}y=y{+}_{G}x\right\}$$
9	2 4 8	3eqtr2i	$$⊢Z=\left\{x\in B|\forall y\in Bx{+}_{G}y=y{+}_{G}x\right\}$$
10	1 6	cmncom	$$⊢\left(G\in \mathrm{CMnd}\wedge x\in B\wedge y\in B\right)\to x{+}_{G}y=y{+}_{G}x$$
11	10	3expa	$$⊢\left(\left(G\in \mathrm{CMnd}\wedge x\in B\right)\wedge y\in B\right)\to x{+}_{G}y=y{+}_{G}x$$
12	11	ralrimiva	$$⊢\left(G\in \mathrm{CMnd}\wedge x\in B\right)\to \forall y\in Bx{+}_{G}y=y{+}_{G}x$$
13	12	rabeqcda	$$⊢G\in \mathrm{CMnd}\to \left\{x\in B|\forall y\in Bx{+}_{G}y=y{+}_{G}x\right\}=B$$
14	9 13	eqtr2id	$$⊢G\in \mathrm{CMnd}\to B=Z$$