This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubDRing ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → 𝑅 ∈ DivRing )
2 simp2 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) )
3 issdrg ⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑠 ) ∈ DivRing ) )
4 3 simp2bi ⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) → 𝑠 ∈ ( SubRing ‘ 𝑅 ) )
5 4 ssriv ⊢ ( SubDRing ‘ 𝑅 ) ⊆ ( SubRing ‘ 𝑅 )
6 2 5 sstrdi ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ⊆ ( SubRing ‘ 𝑅 ) )
7 simp3 ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ≠ ∅ )
8 subrgint ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
9 6 7 8 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
10 eqid ⊢ ( 𝑅 ↾s ∩ 𝑆 ) = ( 𝑅 ↾s ∩ 𝑆 )
11 2 sselda ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ ( SubDRing ‘ 𝑅 ) )
12 3 simp3bi ⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑠 ) ∈ DivRing )
13 11 12 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑅 ↾s 𝑠 ) ∈ DivRing )
14 10 1 6 7 13 subdrgint ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ( 𝑅 ↾s ∩ 𝑆 ) ∈ DivRing )
15 issdrg ⊢ ( ∩ 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ ∩ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s ∩ 𝑆 ) ∈ DivRing ) )
16 1 9 14 15 syl3anbrc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ⊆ ( SubDRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubDRing ‘ 𝑅 ) )