# Metamath Proof Explorer

## Theorem subrgacs

Description: Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypothesis subrgacs.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
Assertion subrgacs ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubRing}\left({R}\right)\in \mathrm{ACS}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 subrgacs.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
3 2 issubrg3 ${⊢}{R}\in \mathrm{Ring}\to \left({x}\in \mathrm{SubRing}\left({R}\right)↔\left({x}\in \mathrm{SubGrp}\left({R}\right)\wedge {x}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\right)\right)$
4 elin ${⊢}{x}\in \left(\mathrm{SubGrp}\left({R}\right)\cap \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\right)↔\left({x}\in \mathrm{SubGrp}\left({R}\right)\wedge {x}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\right)$
5 3 4 syl6bbr ${⊢}{R}\in \mathrm{Ring}\to \left({x}\in \mathrm{SubRing}\left({R}\right)↔{x}\in \left(\mathrm{SubGrp}\left({R}\right)\cap \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\right)\right)$
6 5 eqrdv ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubRing}\left({R}\right)=\mathrm{SubGrp}\left({R}\right)\cap \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)$
7 1 fvexi ${⊢}{B}\in \mathrm{V}$
8 mreacs ${⊢}{B}\in \mathrm{V}\to \mathrm{ACS}\left({B}\right)\in \mathrm{Moore}\left(𝒫{B}\right)$
9 7 8 mp1i ${⊢}{R}\in \mathrm{Ring}\to \mathrm{ACS}\left({B}\right)\in \mathrm{Moore}\left(𝒫{B}\right)$
10 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
11 1 subgacs ${⊢}{R}\in \mathrm{Grp}\to \mathrm{SubGrp}\left({R}\right)\in \mathrm{ACS}\left({B}\right)$
12 10 11 syl ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubGrp}\left({R}\right)\in \mathrm{ACS}\left({B}\right)$
13 2 ringmgp ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{R}}\in \mathrm{Mnd}$
14 2 1 mgpbas ${⊢}{B}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{R}}}$
15 14 submacs ${⊢}{\mathrm{mulGrp}}_{{R}}\in \mathrm{Mnd}\to \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\in \mathrm{ACS}\left({B}\right)$
16 13 15 syl ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\in \mathrm{ACS}\left({B}\right)$
17 mreincl ${⊢}\left(\mathrm{ACS}\left({B}\right)\in \mathrm{Moore}\left(𝒫{B}\right)\wedge \mathrm{SubGrp}\left({R}\right)\in \mathrm{ACS}\left({B}\right)\wedge \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\in \mathrm{ACS}\left({B}\right)\right)\to \mathrm{SubGrp}\left({R}\right)\cap \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\in \mathrm{ACS}\left({B}\right)$
18 9 12 16 17 syl3anc ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubGrp}\left({R}\right)\cap \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{R}}\right)\in \mathrm{ACS}\left({B}\right)$
19 6 18 eqeltrd ${⊢}{R}\in \mathrm{Ring}\to \mathrm{SubRing}\left({R}\right)\in \mathrm{ACS}\left({B}\right)$