# Metamath Proof Explorer

## Theorem subrgint

Description: The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014) (Revised by Mario Carneiro, 7-Dec-2014)

Ref Expression
Assertion subrgint ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \bigcap {S}\in \mathrm{SubRing}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 subrgsubg ${⊢}{r}\in \mathrm{SubRing}\left({R}\right)\to {r}\in \mathrm{SubGrp}\left({R}\right)$
2 1 ssriv ${⊢}\mathrm{SubRing}\left({R}\right)\subseteq \mathrm{SubGrp}\left({R}\right)$
3 sstr ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge \mathrm{SubRing}\left({R}\right)\subseteq \mathrm{SubGrp}\left({R}\right)\right)\to {S}\subseteq \mathrm{SubGrp}\left({R}\right)$
4 2 3 mpan2 ${⊢}{S}\subseteq \mathrm{SubRing}\left({R}\right)\to {S}\subseteq \mathrm{SubGrp}\left({R}\right)$
5 subgint ${⊢}\left({S}\subseteq \mathrm{SubGrp}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \bigcap {S}\in \mathrm{SubGrp}\left({R}\right)$
6 4 5 sylan ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \bigcap {S}\in \mathrm{SubGrp}\left({R}\right)$
7 ssel2 ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {r}\in {S}\right)\to {r}\in \mathrm{SubRing}\left({R}\right)$
8 7 adantlr ${⊢}\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge {r}\in {S}\right)\to {r}\in \mathrm{SubRing}\left({R}\right)$
9 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
10 9 subrg1cl ${⊢}{r}\in \mathrm{SubRing}\left({R}\right)\to {1}_{{R}}\in {r}$
11 8 10 syl ${⊢}\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge {r}\in {S}\right)\to {1}_{{R}}\in {r}$
12 11 ralrimiva ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \forall {r}\in {S}\phantom{\rule{.4em}{0ex}}{1}_{{R}}\in {r}$
13 fvex ${⊢}{1}_{{R}}\in \mathrm{V}$
14 13 elint2 ${⊢}{1}_{{R}}\in \bigcap {S}↔\forall {r}\in {S}\phantom{\rule{.4em}{0ex}}{1}_{{R}}\in {r}$
15 12 14 sylibr ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to {1}_{{R}}\in \bigcap {S}$
16 8 adantlr ${⊢}\left(\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge \left({x}\in \bigcap {S}\wedge {y}\in \bigcap {S}\right)\right)\wedge {r}\in {S}\right)\to {r}\in \mathrm{SubRing}\left({R}\right)$
17 simprl ${⊢}\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge \left({x}\in \bigcap {S}\wedge {y}\in \bigcap {S}\right)\right)\to {x}\in \bigcap {S}$
18 elinti ${⊢}{x}\in \bigcap {S}\to \left({r}\in {S}\to {x}\in {r}\right)$
19 18 imp ${⊢}\left({x}\in \bigcap {S}\wedge {r}\in {S}\right)\to {x}\in {r}$
20 17 19 sylan ${⊢}\left(\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge \left({x}\in \bigcap {S}\wedge {y}\in \bigcap {S}\right)\right)\wedge {r}\in {S}\right)\to {x}\in {r}$
21 simprr ${⊢}\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge \left({x}\in \bigcap {S}\wedge {y}\in \bigcap {S}\right)\right)\to {y}\in \bigcap {S}$
22 elinti ${⊢}{y}\in \bigcap {S}\to \left({r}\in {S}\to {y}\in {r}\right)$
23 22 imp ${⊢}\left({y}\in \bigcap {S}\wedge {r}\in {S}\right)\to {y}\in {r}$
24 21 23 sylan ${⊢}\left(\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge \left({x}\in \bigcap {S}\wedge {y}\in \bigcap {S}\right)\right)\wedge {r}\in {S}\right)\to {y}\in {r}$
25 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
26 25 subrgmcl ${⊢}\left({r}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in {r}\wedge {y}\in {r}\right)\to {x}{\cdot }_{{R}}{y}\in {r}$
27 16 20 24 26 syl3anc ${⊢}\left(\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge \left({x}\in \bigcap {S}\wedge {y}\in \bigcap {S}\right)\right)\wedge {r}\in {S}\right)\to {x}{\cdot }_{{R}}{y}\in {r}$
28 27 ralrimiva ${⊢}\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge \left({x}\in \bigcap {S}\wedge {y}\in \bigcap {S}\right)\right)\to \forall {r}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {r}$
29 ovex ${⊢}{x}{\cdot }_{{R}}{y}\in \mathrm{V}$
30 29 elint2 ${⊢}{x}{\cdot }_{{R}}{y}\in \bigcap {S}↔\forall {r}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in {r}$
31 28 30 sylibr ${⊢}\left(\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge \left({x}\in \bigcap {S}\wedge {y}\in \bigcap {S}\right)\right)\to {x}{\cdot }_{{R}}{y}\in \bigcap {S}$
32 31 ralrimivva ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \forall {x}\in \bigcap {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcap {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in \bigcap {S}$
33 ssn0 ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \mathrm{SubRing}\left({R}\right)\ne \varnothing$
34 n0 ${⊢}\mathrm{SubRing}\left({R}\right)\ne \varnothing ↔\exists {r}\phantom{\rule{.4em}{0ex}}{r}\in \mathrm{SubRing}\left({R}\right)$
35 subrgrcl ${⊢}{r}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Ring}$
36 35 exlimiv ${⊢}\exists {r}\phantom{\rule{.4em}{0ex}}{r}\in \mathrm{SubRing}\left({R}\right)\to {R}\in \mathrm{Ring}$
37 34 36 sylbi ${⊢}\mathrm{SubRing}\left({R}\right)\ne \varnothing \to {R}\in \mathrm{Ring}$
38 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
39 38 9 25 issubrg2 ${⊢}{R}\in \mathrm{Ring}\to \left(\bigcap {S}\in \mathrm{SubRing}\left({R}\right)↔\left(\bigcap {S}\in \mathrm{SubGrp}\left({R}\right)\wedge {1}_{{R}}\in \bigcap {S}\wedge \forall {x}\in \bigcap {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcap {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in \bigcap {S}\right)\right)$
40 33 37 39 3syl ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \left(\bigcap {S}\in \mathrm{SubRing}\left({R}\right)↔\left(\bigcap {S}\in \mathrm{SubGrp}\left({R}\right)\wedge {1}_{{R}}\in \bigcap {S}\wedge \forall {x}\in \bigcap {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in \bigcap {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{R}}{y}\in \bigcap {S}\right)\right)$
41 6 15 32 40 mpbir3and ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \bigcap {S}\in \mathrm{SubRing}\left({R}\right)$