This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 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 )