# 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}={\mathrm{mulGrp}}_{{R}}$
Assertion issubrg3 ${⊢}{R}\in \mathrm{Ring}\to \left({S}\in \mathrm{SubRing}\left({R}\right)↔\left({S}\in \mathrm{SubGrp}\left({R}\right)\wedge {S}\in \mathrm{SubMnd}\left({M}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 issubrg3.m ${⊢}{M}={\mathrm{mulGrp}}_{{R}}$
2 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
3 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
4 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
5 2 3 4 issubrg2 ${⊢}{R}\in \mathrm{Ring}\to \left({S}\in \mathrm{SubRing}\left({R}\right)↔\left({S}\in \mathrm{SubGrp}\left({R}\right)\wedge {1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)$
6 3anass ${⊢}\left({S}\in \mathrm{SubGrp}\left({R}\right)\wedge {1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)↔\left({S}\in \mathrm{SubGrp}\left({R}\right)\wedge \left({1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)$
7 5 6 syl6bb ${⊢}{R}\in \mathrm{Ring}\to \left({S}\in \mathrm{SubRing}\left({R}\right)↔\left({S}\in \mathrm{SubGrp}\left({R}\right)\wedge \left({1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)\right)$
8 1 ringmgp ${⊢}{R}\in \mathrm{Ring}\to {M}\in \mathrm{Mnd}$
9 2 subgss ${⊢}{S}\in \mathrm{SubGrp}\left({R}\right)\to {S}\subseteq {\mathrm{Base}}_{{R}}$
10 1 2 mgpbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{M}}$
11 1 3 ringidval ${⊢}{1}_{{R}}={0}_{{M}}$
12 1 4 mgpplusg ${⊢}{\cdot }_{{R}}={+}_{{M}}$
13 10 11 12 issubm ${⊢}{M}\in \mathrm{Mnd}\to \left({S}\in \mathrm{SubMnd}\left({M}\right)↔\left({S}\subseteq {\mathrm{Base}}_{{R}}\wedge {1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)$
14 3anass ${⊢}\left({S}\subseteq {\mathrm{Base}}_{{R}}\wedge {1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)↔\left({S}\subseteq {\mathrm{Base}}_{{R}}\wedge \left({1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)$
15 13 14 syl6bb ${⊢}{M}\in \mathrm{Mnd}\to \left({S}\in \mathrm{SubMnd}\left({M}\right)↔\left({S}\subseteq {\mathrm{Base}}_{{R}}\wedge \left({1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)\right)$
16 15 baibd ${⊢}\left({M}\in \mathrm{Mnd}\wedge {S}\subseteq {\mathrm{Base}}_{{R}}\right)\to \left({S}\in \mathrm{SubMnd}\left({M}\right)↔\left({1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)$
17 8 9 16 syl2an ${⊢}\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{SubGrp}\left({R}\right)\right)\to \left({S}\in \mathrm{SubMnd}\left({M}\right)↔\left({1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)$
18 17 pm5.32da ${⊢}{R}\in \mathrm{Ring}\to \left(\left({S}\in \mathrm{SubGrp}\left({R}\right)\wedge {S}\in \mathrm{SubMnd}\left({M}\right)\right)↔\left({S}\in \mathrm{SubGrp}\left({R}\right)\wedge \left({1}_{{R}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {S}\right)\right)\right)$
19 7 18 bitr4d ${⊢}{R}\in \mathrm{Ring}\to \left({S}\in \mathrm{SubRing}\left({R}\right)↔\left({S}\in \mathrm{SubGrp}\left({R}\right)\wedge {S}\in \mathrm{SubMnd}\left({M}\right)\right)\right)$