# Metamath Proof Explorer

## Theorem sdrgint

Description: The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023)

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

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to {R}\in \mathrm{DivRing}$
2 simp2 ${⊢}\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to {S}\subseteq \mathrm{SubDRing}\left({R}\right)$
3 issdrg ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge {s}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right)$
4 3 simp2bi ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)\to {s}\in \mathrm{SubRing}\left({R}\right)$
5 4 ssriv ${⊢}\mathrm{SubDRing}\left({R}\right)\subseteq \mathrm{SubRing}\left({R}\right)$
6 2 5 sstrdi ${⊢}\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to {S}\subseteq \mathrm{SubRing}\left({R}\right)$
7 simp3 ${⊢}\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to {S}\ne \varnothing$
8 subrgint ${⊢}\left({S}\subseteq \mathrm{SubRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \bigcap {S}\in \mathrm{SubRing}\left({R}\right)$
9 6 7 8 syl2anc ${⊢}\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \bigcap {S}\in \mathrm{SubRing}\left({R}\right)$
10 eqid ${⊢}{R}{↾}_{𝑠}\bigcap {S}={R}{↾}_{𝑠}\bigcap {S}$
11 2 sselda ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge {s}\in {S}\right)\to {s}\in \mathrm{SubDRing}\left({R}\right)$
12 3 simp3bi ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)\to {R}{↾}_{𝑠}{s}\in \mathrm{DivRing}$
13 11 12 syl ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\wedge {s}\in {S}\right)\to {R}{↾}_{𝑠}{s}\in \mathrm{DivRing}$
14 10 1 6 7 13 subdrgint ${⊢}\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to {R}{↾}_{𝑠}\bigcap {S}\in \mathrm{DivRing}$
15 issdrg ${⊢}\bigcap {S}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge \bigcap {S}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}\bigcap {S}\in \mathrm{DivRing}\right)$
16 1 9 14 15 syl3anbrc ${⊢}\left({R}\in \mathrm{DivRing}\wedge {S}\subseteq \mathrm{SubDRing}\left({R}\right)\wedge {S}\ne \varnothing \right)\to \bigcap {S}\in \mathrm{SubDRing}\left({R}\right)$