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 Ring S SubRing R S SubGrp R S SubMnd M

Proof

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