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 )