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 = ( Base ` G )
	crngbascntr.z	|- Z = ( Cntr ` ( mulGrp ` G ) )
Assertion	crngbascntr	|- ( G e. CRing -> B = Z )

Proof

Step	Hyp	Ref	Expression
1		crngbascntr.b	|- B = ( Base ` G )
2		crngbascntr.z	|- Z = ( Cntr ` ( mulGrp ` G ) )
3		eqid	|- ( mulGrp ` G ) = ( mulGrp ` G )
4	3	crngmgp	|- ( G e. CRing -> ( mulGrp ` G ) e. CMnd )
5	3 1	mgpbas	|- B = ( Base ` ( mulGrp ` G ) )
6	5 2	cmnbascntr	|- ( ( mulGrp ` G ) e. CMnd -> B = Z )
7	4 6	syl	|- ( G e. CRing -> B = Z )