Theorem crngbascntr

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

	Ref	Expression
Hypotheses	crngbascntr.b	$$⊢B={\mathrm{Base}}_G$$
	crngbascntr.z	$$⊢Z=\mathrm{Cntr}\left({\mathrm{mulGrp}}_G\right)$$
Assertion	crngbascntr	$$⊢G\in \mathrm{CRing}\to B=Z$$

Proof

Step	Hyp	Ref	Expression
1		crngbascntr.b	$$⊢B={\mathrm{Base}}_G$$
2		crngbascntr.z	$$⊢Z=\mathrm{Cntr}\left({\mathrm{mulGrp}}_G\right)$$
3		eqid	$$⊢{\mathrm{mulGrp}}_G={\mathrm{mulGrp}}_G$$
4	3	crngmgp	$$⊢G\in \mathrm{CRing}\to {\mathrm{mulGrp}}_G\in \mathrm{CMnd}$$
5	3 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_G}$$
6	5 2	cmnbascntr	$$⊢{\mathrm{mulGrp}}_G\in \mathrm{CMnd}\to B=Z$$
7	4 6	syl	$$⊢G\in \mathrm{CRing}\to B=Z$$