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 ‘ 𝑅 ) )