Theorem cntrcrng

Description: The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023)

	Ref	Expression
Hypothesis	cntrcrng.z	|- Z = ( R |`s ( Cntr ` ( mulGrp ` R ) ) )
Assertion	cntrcrng	|- ( R e. Ring -> Z e. CRing )

Proof

Step	Hyp	Ref	Expression
1		cntrcrng.z	|- Z = ( R |`s ( Cntr ` ( mulGrp ` R ) ) )
2		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
3		eqid	|- ( Base ` R ) = ( Base ` R )
4	2 3	mgpbas	|- ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
5		eqid	|- ( Cntz ` ( mulGrp ` R ) ) = ( Cntz ` ( mulGrp ` R ) )
6	4 5	cntrval	|- ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) = ( Cntr ` ( mulGrp ` R ) )
7		ssid	|- ( Base ` R ) C_ ( Base ` R )
8	3 2 5	cntzsubr	|- ( ( R e. Ring /\ ( Base ` R ) C_ ( Base ` R ) ) -> ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) e. ( SubRing ` R ) )
9	7 8	mpan2	|- ( R e. Ring -> ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) e. ( SubRing ` R ) )
10	6 9	eqeltrrid	|- ( R e. Ring -> ( Cntr ` ( mulGrp ` R ) ) e. ( SubRing ` R ) )
11	1	subrgring	|- ( ( Cntr ` ( mulGrp ` R ) ) e. ( SubRing ` R ) -> Z e. Ring )
12	10 11	syl	|- ( R e. Ring -> Z e. Ring )
13		fvex	|- ( Cntr ` ( mulGrp ` R ) ) e. _V
14	1 2	mgpress	|- ( ( R e. Ring /\ ( Cntr ` ( mulGrp ` R ) ) e. _V ) -> ( ( mulGrp ` R ) |`s ( Cntr ` ( mulGrp ` R ) ) ) = ( mulGrp ` Z ) )
15	13 14	mpan2	|- ( R e. Ring -> ( ( mulGrp ` R ) |`s ( Cntr ` ( mulGrp ` R ) ) ) = ( mulGrp ` Z ) )
16	2	ringmgp	|- ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
17		eqid	|- ( ( mulGrp ` R ) |`s ( Cntr ` ( mulGrp ` R ) ) ) = ( ( mulGrp ` R ) |`s ( Cntr ` ( mulGrp ` R ) ) )
18	17	cntrcmnd	|- ( ( mulGrp ` R ) e. Mnd -> ( ( mulGrp ` R ) |`s ( Cntr ` ( mulGrp ` R ) ) ) e. CMnd )
19	16 18	syl	|- ( R e. Ring -> ( ( mulGrp ` R ) |`s ( Cntr ` ( mulGrp ` R ) ) ) e. CMnd )
20	15 19	eqeltrrd	|- ( R e. Ring -> ( mulGrp ` Z ) e. CMnd )
21		eqid	|- ( mulGrp ` Z ) = ( mulGrp ` Z )
22	21	iscrng	|- ( Z e. CRing <-> ( Z e. Ring /\ ( mulGrp ` Z ) e. CMnd ) )
23	12 20 22	sylanbrc	|- ( R e. Ring -> Z e. CRing )