Theorem elmgpcntrd

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

	Ref	Expression
Hypotheses	elmgpcntrd.b	$$⊢B={\mathrm{Base}}_R$$
	elmgpcntrd.m	$$⊢M={\mathrm{mulGrp}}_R$$
	elmgpcntrd.z	$$⊢Z=\mathrm{Cntr}\left(M\right)$$
	elmgpcntrd.x	$$⊢\phi \to X\in B$$
	elmgpcntrd.y	$$⊢\left(\phi \wedge y\in B\right)\to X{\cdot }_{R}y=y{\cdot }_{R}X$$
Assertion	elmgpcntrd	$$⊢\phi \to X\in Z$$

Proof

Step	Hyp	Ref	Expression
1		elmgpcntrd.b	$$⊢B={\mathrm{Base}}_R$$
2		elmgpcntrd.m	$$⊢M={\mathrm{mulGrp}}_R$$
3		elmgpcntrd.z	$$⊢Z=\mathrm{Cntr}\left(M\right)$$
4		elmgpcntrd.x	$$⊢\phi \to X\in B$$
5		elmgpcntrd.y	$$⊢\left(\phi \wedge y\in B\right)\to X{\cdot }_{R}y=y{\cdot }_{R}X$$
6	5	ralrimiva	$$⊢\phi \to \forall y\in BX{\cdot }_{R}y=y{\cdot }_{R}X$$
7	2 1	mgpbas	$$⊢B={\mathrm{Base}}_M$$
8		eqid	$$⊢{\cdot }_R={\cdot }_R$$
9	2 8	mgpplusg	$$⊢{\cdot }_R={+}_M$$
10	7 9 3	elcntr	$$⊢X\in Z\leftrightarrow \left(X\in B\wedge \forall y\in BX{\cdot }_{R}y=y{\cdot }_{R}X\right)$$
11	4 6 10	sylanbrc	$$⊢\phi \to X\in Z$$