Metamath Proof Explorer

Theorem issubrg3

Description: A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis issubrg3.m 
|- M = ( mulGrp ` R )
Assertion issubrg3 
|- ( R e. Ring -> ( S e. ( SubRing ` R ) <-> ( S e. ( SubGrp ` R ) /\ S e. ( SubMnd ` M ) ) ) )

Proof

Step Hyp Ref Expression
1 issubrg3.m 
 |-  M = ( mulGrp ` R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
4 eqid 
 |-  ( .r ` R ) = ( .r ` R )
5 2 3 4 issubrg2 
 |-  ( R e. Ring -> ( S e. ( SubRing ` R ) <-> ( S e. ( SubGrp ` R ) /\ ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) )
6 3anass 
 |-  ( ( S e. ( SubGrp ` R ) /\ ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) <-> ( S e. ( SubGrp ` R ) /\ ( ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) )
7 5 6 bitrdi 
 |-  ( R e. Ring -> ( S e. ( SubRing ` R ) <-> ( S e. ( SubGrp ` R ) /\ ( ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) ) )
8 1 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
9 2 subgss 
 |-  ( S e. ( SubGrp ` R ) -> S C_ ( Base ` R ) )
10 1 2 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
11 1 3 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
12 1 4 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
13 10 11 12 issubm 
 |-  ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ ( Base ` R ) /\ ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) )
14 3anass 
 |-  ( ( S C_ ( Base ` R ) /\ ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) <-> ( S C_ ( Base ` R ) /\ ( ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) )
15 13 14 bitrdi 
 |-  ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ ( Base ` R ) /\ ( ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) ) )
16 15 baibd 
 |-  ( ( M e. Mnd /\ S C_ ( Base ` R ) ) -> ( S e. ( SubMnd ` M ) <-> ( ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) )
17 8 9 16 syl2an 
 |-  ( ( R e. Ring /\ S e. ( SubGrp ` R ) ) -> ( S e. ( SubMnd ` M ) <-> ( ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) )
18 17 pm5.32da 
 |-  ( R e. Ring -> ( ( S e. ( SubGrp ` R ) /\ S e. ( SubMnd ` M ) ) <-> ( S e. ( SubGrp ` R ) /\ ( ( 1r ` R ) e. S /\ A. x e. S A. y e. S ( x ( .r ` R ) y ) e. S ) ) ) )
19 7 18 bitr4d 
 |-  ( R e. Ring -> ( S e. ( SubRing ` R ) <-> ( S e. ( SubGrp ` R ) /\ S e. ( SubMnd ` M ) ) ) )