Theorem elmgpcntrd

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

	Ref	Expression
Hypotheses	elmgpcntrd.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	elmgpcntrd.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	elmgpcntrd.z	⊢ 𝑍 = ( Cntr ‘ 𝑀 )
	elmgpcntrd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	elmgpcntrd.y	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
Assertion	elmgpcntrd	⊢ ( 𝜑 → 𝑋 ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		elmgpcntrd.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		elmgpcntrd.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
3		elmgpcntrd.z	⊢ 𝑍 = ( Cntr ‘ 𝑀 )
4		elmgpcntrd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		elmgpcntrd.y	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
6	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( 𝑋 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
7	2 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
8		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9	2 8	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
10	7 9 3	elcntr	⊢ ( 𝑋 ∈ 𝑍 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑋 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) )
11	4 6 10	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ 𝑍 )