Metamath Proof Explorer

Theorem subrgcrng

Description: A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypothesis subrgring.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
Assertion subrgcrng ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑆 ∈ CRing )

Proof

Step Hyp Ref Expression
1 subrgring.1 ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 1 subrgring ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
3 2 adantl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑆 ∈ Ring )
4 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5 1 4 mgpress ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 ) = ( mulGrp ‘ 𝑆 ) )
6 4 crngmgp ⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
7 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
8 7 ringmgp ⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
9 3 8 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
10 5 9 eqeltrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 ) ∈ Mnd )
11 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 ) = ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 )
12 11 subcmn ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ∧ ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 ) ∈ Mnd ) → ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 ) ∈ CMnd )
13 6 10 12 syl2an2r ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s 𝐴 ) ∈ CMnd )
14 5 13 eqeltrrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → ( mulGrp ‘ 𝑆 ) ∈ CMnd )
15 7 iscrng ⊢ ( 𝑆 ∈ CRing ↔ ( 𝑆 ∈ Ring ∧ ( mulGrp ‘ 𝑆 ) ∈ CMnd ) )
16 3 14 15 sylanbrc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑆 ∈ CRing )