Theorem elmgpcntrd

Description: The center of a ring. (Contributed by Zhi Wang, 11-Sep-2025)

	Ref	Expression
Hypotheses	elmgpcntrd.b	|- B = ( Base ` R )
	elmgpcntrd.m	|- M = ( mulGrp ` R )
	elmgpcntrd.z	|- Z = ( Cntr ` M )
	elmgpcntrd.x	|- ( ph -> X e. B )
	elmgpcntrd.y	|- ( ( ph /\ y e. B ) -> ( X ( .r ` R ) y ) = ( y ( .r ` R ) X ) )
Assertion	elmgpcntrd	|- ( ph -> X e. Z )

Proof

Step	Hyp	Ref	Expression
1		elmgpcntrd.b	|- B = ( Base ` R )
2		elmgpcntrd.m	|- M = ( mulGrp ` R )
3		elmgpcntrd.z	|- Z = ( Cntr ` M )
4		elmgpcntrd.x	|- ( ph -> X e. B )
5		elmgpcntrd.y	|- ( ( ph /\ y e. B ) -> ( X ( .r ` R ) y ) = ( y ( .r ` R ) X ) )
6	5	ralrimiva	|- ( ph -> A. y e. B ( X ( .r ` R ) y ) = ( y ( .r ` R ) X ) )
7	2 1	mgpbas	|- B = ( Base ` M )
8		eqid	|- ( .r ` R ) = ( .r ` R )
9	2 8	mgpplusg	|- ( .r ` R ) = ( +g ` M )
10	7 9 3	elcntr	|- ( X e. Z <-> ( X e. B /\ A. y e. B ( X ( .r ` R ) y ) = ( y ( .r ` R ) X ) ) )
11	4 6 10	sylanbrc	|- ( ph -> X e. Z )