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=mulGrpR
Assertion issubrg3 RRingSSubRingRSSubGrpRSSubMndM

Proof

Step Hyp Ref Expression
1 issubrg3.m M=mulGrpR
2 eqid BaseR=BaseR
3 eqid 1R=1R
4 eqid R=R
5 2 3 4 issubrg2 RRingSSubRingRSSubGrpR1RSxSySxRyS
6 3anass SSubGrpR1RSxSySxRySSSubGrpR1RSxSySxRyS
7 5 6 bitrdi RRingSSubRingRSSubGrpR1RSxSySxRyS
8 1 ringmgp RRingMMnd
9 2 subgss SSubGrpRSBaseR
10 1 2 mgpbas BaseR=BaseM
11 1 3 ringidval 1R=0M
12 1 4 mgpplusg R=+M
13 10 11 12 issubm MMndSSubMndMSBaseR1RSxSySxRyS
14 3anass SBaseR1RSxSySxRySSBaseR1RSxSySxRyS
15 13 14 bitrdi MMndSSubMndMSBaseR1RSxSySxRyS
16 15 baibd MMndSBaseRSSubMndM1RSxSySxRyS
17 8 9 16 syl2an RRingSSubGrpRSSubMndM1RSxSySxRyS
18 17 pm5.32da RRingSSubGrpRSSubMndMSSubGrpR1RSxSySxRyS
19 7 18 bitr4d RRingSSubRingRSSubGrpRSSubMndM