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 = ( R |`s A )
Assertion	subrgcrng	|- ( ( R e. CRing /\ A e. ( SubRing ` R ) ) -> S e. CRing )

Proof

Step	Hyp	Ref	Expression
1		subrgring.1	|- S = ( R |`s A )
2	1	subrgring	|- ( A e. ( SubRing ` R ) -> S e. Ring )
3	2	adantl	|- ( ( R e. CRing /\ A e. ( SubRing ` R ) ) -> S e. Ring )
4		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
5	1 4	mgpress	|- ( ( R e. CRing /\ A e. ( SubRing ` R ) ) -> ( ( mulGrp ` R ) |`s A ) = ( mulGrp ` S ) )
6	4	crngmgp	|- ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
7		eqid	|- ( mulGrp ` S ) = ( mulGrp ` S )
8	7	ringmgp	|- ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
9	3 8	syl	|- ( ( R e. CRing /\ A e. ( SubRing ` R ) ) -> ( mulGrp ` S ) e. Mnd )
10	5 9	eqeltrd	|- ( ( R e. CRing /\ A e. ( SubRing ` R ) ) -> ( ( mulGrp ` R ) |`s A ) e. Mnd )
11		eqid	|- ( ( mulGrp ` R ) |`s A ) = ( ( mulGrp ` R ) |`s A )
12	11	subcmn	|- ( ( ( mulGrp ` R ) e. CMnd /\ ( ( mulGrp ` R ) |`s A ) e. Mnd ) -> ( ( mulGrp ` R ) |`s A ) e. CMnd )
13	6 10 12	syl2an2r	|- ( ( R e. CRing /\ A e. ( SubRing ` R ) ) -> ( ( mulGrp ` R ) |`s A ) e. CMnd )
14	5 13	eqeltrrd	|- ( ( R e. CRing /\ A e. ( SubRing ` R ) ) -> ( mulGrp ` S ) e. CMnd )
15	7	iscrng	|- ( S e. CRing <-> ( S e. Ring /\ ( mulGrp ` S ) e. CMnd ) )
16	3 14 15	sylanbrc	|- ( ( R e. CRing /\ A e. ( SubRing ` R ) ) -> S e. CRing )