Metamath Proof Explorer

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 ↾ 𝑠 Cntr ⁡ mulGrp R
Assertion cntrcrng ⊢ R ∈ Ring → Z ∈ 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 ⊆ Base R
8 3 2 5 cntzsubr ⊢ R ∈ Ring ∧ Base R ⊆ Base R → Cntz ⁡ mulGrp R ⁡ Base R ∈ SubRing ⁡ R
9 7 8 mpan2 ⊢ R ∈ Ring → Cntz ⁡ mulGrp R ⁡ Base R ∈ SubRing ⁡ R
10 6 9 eqeltrrid ⊢ R ∈ Ring → Cntr ⁡ mulGrp R ∈ SubRing ⁡ R
11 1 subrgring ⊢ Cntr ⁡ mulGrp R ∈ SubRing ⁡ R → Z ∈ Ring
12 10 11 syl ⊢ R ∈ Ring → Z ∈ Ring
13 fvex ⊢ Cntr ⁡ mulGrp R ∈ V
14 1 2 mgpress ⊢ R ∈ Ring ∧ Cntr ⁡ mulGrp R ∈ V → mulGrp R ↾ 𝑠 Cntr ⁡ mulGrp R = mulGrp Z
15 13 14 mpan2 ⊢ R ∈ Ring → mulGrp R ↾ 𝑠 Cntr ⁡ mulGrp R = mulGrp Z
16 2 ringmgp ⊢ R ∈ Ring → mulGrp R ∈ Mnd
17 eqid ⊢ mulGrp R ↾ 𝑠 Cntr ⁡ mulGrp R = mulGrp R ↾ 𝑠 Cntr ⁡ mulGrp R
18 17 cntrcmnd ⊢ mulGrp R ∈ Mnd → mulGrp R ↾ 𝑠 Cntr ⁡ mulGrp R ∈ CMnd
19 16 18 syl ⊢ R ∈ Ring → mulGrp R ↾ 𝑠 Cntr ⁡ mulGrp R ∈ CMnd
20 15 19 eqeltrrd ⊢ R ∈ Ring → mulGrp Z ∈ CMnd
21 eqid ⊢ mulGrp Z = mulGrp Z
22 21 iscrng ⊢ Z ∈ CRing ↔ Z ∈ Ring ∧ mulGrp Z ∈ CMnd
23 12 20 22 sylanbrc ⊢ R ∈ Ring → Z ∈ CRing