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 ⊢ 𝑍 = ( 𝑅 ↾s ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) )
Assertion cntrcrng ( 𝑅 ∈ Ring → 𝑍 ∈ CRing )

Proof

Step Hyp Ref Expression
1 cntrcrng.z ⊢ 𝑍 = ( 𝑅 ↾s ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) )
2 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 2 3 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
5 eqid ⊢ ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) = ( Cntz ‘ ( mulGrp ‘ 𝑅 ) )
6 4 5 cntrval ⊢ ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) = ( Cntr ‘ ( mulGrp ‘ 𝑅 ) )
7 ssid ⊢ ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 )
8 3 2 5 cntzsubr ⊢ ( ( 𝑅 ∈ Ring ∧ ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) ∈ ( SubRing ‘ 𝑅 ) )
9 7 8 mpan2 ⊢ ( 𝑅 ∈ Ring → ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) ∈ ( SubRing ‘ 𝑅 ) )
10 6 9 eqeltrrid ⊢ ( 𝑅 ∈ Ring → ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( SubRing ‘ 𝑅 ) )
11 1 subrgring ⊢ ( ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( SubRing ‘ 𝑅 ) → 𝑍 ∈ Ring )
12 10 11 syl ⊢ ( 𝑅 ∈ Ring → 𝑍 ∈ Ring )
13 fvex ⊢ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ∈ V
14 1 2 mgpress ⊢ ( ( 𝑅 ∈ Ring ∧ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ∈ V ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( mulGrp ‘ 𝑍 ) )
15 13 14 mpan2 ⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ↾s ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( mulGrp ‘ 𝑍 ) )
16 2 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
17 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) )
18 17 cntrcmnd ⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → ( ( mulGrp ‘ 𝑅 ) ↾s ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ) ∈ CMnd )
19 16 18 syl ⊢ ( 𝑅 ∈ Ring → ( ( mulGrp ‘ 𝑅 ) ↾s ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ) ∈ CMnd )
20 15 19 eqeltrrd ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑍 ) ∈ CMnd )
21 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
22 21 iscrng ⊢ ( 𝑍 ∈ CRing ↔ ( 𝑍 ∈ Ring ∧ ( mulGrp ‘ 𝑍 ) ∈ CMnd ) )
23 12 20 22 sylanbrc ⊢ ( 𝑅 ∈ Ring → 𝑍 ∈ CRing )