Metamath Proof Explorer

Theorem subrgsubm

Description: A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis subrgsubm.1 
|- M = ( mulGrp ` R )
Assertion subrgsubm 
|- ( A e. ( SubRing ` R ) -> A e. ( SubMnd ` M ) )

Proof

Step Hyp Ref Expression
1 subrgsubm.1 
 |-  M = ( mulGrp ` R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 2 subrgss 
 |-  ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
4 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
5 4 subrg1cl 
 |-  ( A e. ( SubRing ` R ) -> ( 1r ` R ) e. A )
6 subrgrcl 
 |-  ( A e. ( SubRing ` R ) -> R e. Ring )
7 eqid 
 |-  ( R |`s A ) = ( R |`s A )
8 7 1 mgpress 
 |-  ( ( R e. Ring /\ A e. ( SubRing ` R ) ) -> ( M |`s A ) = ( mulGrp ` ( R |`s A ) ) )
9 6 8 mpancom 
 |-  ( A e. ( SubRing ` R ) -> ( M |`s A ) = ( mulGrp ` ( R |`s A ) ) )
10 7 subrgring 
 |-  ( A e. ( SubRing ` R ) -> ( R |`s A ) e. Ring )
11 eqid 
 |-  ( mulGrp ` ( R |`s A ) ) = ( mulGrp ` ( R |`s A ) )
12 11 ringmgp 
 |-  ( ( R |`s A ) e. Ring -> ( mulGrp ` ( R |`s A ) ) e. Mnd )
13 10 12 syl 
 |-  ( A e. ( SubRing ` R ) -> ( mulGrp ` ( R |`s A ) ) e. Mnd )
14 9 13 eqeltrd 
 |-  ( A e. ( SubRing ` R ) -> ( M |`s A ) e. Mnd )
15 1 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
16 1 2 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
17 1 4 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
18 eqid 
 |-  ( M |`s A ) = ( M |`s A )
19 16 17 18 issubm2 
 |-  ( M e. Mnd -> ( A e. ( SubMnd ` M ) <-> ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A /\ ( M |`s A ) e. Mnd ) ) )
20 6 15 19 3syl 
 |-  ( A e. ( SubRing ` R ) -> ( A e. ( SubMnd ` M ) <-> ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A /\ ( M |`s A ) e. Mnd ) ) )
21 3 5 14 20 mpbir3and 
 |-  ( A e. ( SubRing ` R ) -> A e. ( SubMnd ` M ) )