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 ↾_{𝑠} Cntr ({mulGrp}_{R})$
	Assertion	cntrcrng	$⊢ R \in Ring \to Z \in CRing$

Proof

Step	Hyp	Ref	Expression
1		cntrcrng.z	$⊢ Z = R ↾_{𝑠} 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} \subseteq {Base}_{R}$
8	3 2 5	cntzsubr	$⊢ (R \in Ring \land {Base}_{R} \subseteq {Base}_{R}) \to Cntz ({mulGrp}_{R}) ({Base}_{R}) \in SubRing (R)$
9	7 8	mpan2	$⊢ R \in Ring \to Cntz ({mulGrp}_{R}) ({Base}_{R}) \in SubRing (R)$
10	6 9	eqeltrrid	$⊢ R \in Ring \to Cntr ({mulGrp}_{R}) \in SubRing (R)$
11	1	subrgring	$⊢ Cntr ({mulGrp}_{R}) \in SubRing (R) \to Z \in Ring$
12	10 11	syl	$⊢ R \in Ring \to Z \in Ring$
13		fvex	$⊢ Cntr ({mulGrp}_{R}) \in V$
14	1 2	mgpress	$⊢ (R \in Ring \land Cntr ({mulGrp}_{R}) \in V) \to {mulGrp}_{R} ↾_{𝑠} Cntr ({mulGrp}_{R}) = {mulGrp}_{Z}$
15	13 14	mpan2	$⊢ R \in Ring \to {mulGrp}_{R} ↾_{𝑠} Cntr ({mulGrp}_{R}) = {mulGrp}_{Z}$
16	2	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
17		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} Cntr ({mulGrp}_{R}) = {mulGrp}_{R} ↾_{𝑠} Cntr ({mulGrp}_{R})$
18	17	cntrcmnd	$⊢ {mulGrp}_{R} \in Mnd \to {mulGrp}_{R} ↾_{𝑠} Cntr ({mulGrp}_{R}) \in CMnd$
19	16 18	syl	$⊢ R \in Ring \to {mulGrp}_{R} ↾_{𝑠} Cntr ({mulGrp}_{R}) \in CMnd$
20	15 19	eqeltrrd	$⊢ R \in Ring \to {mulGrp}_{Z} \in CMnd$
21		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
22	21	iscrng	$⊢ Z \in CRing \leftrightarrow (Z \in Ring \land {mulGrp}_{Z} \in CMnd)$
23	12 20 22	sylanbrc	$⊢ R \in Ring \to Z \in CRing$

Metamath Proof Explorer

Theorem cntrcrng

Proof