Metamath Proof Explorer

Theorem subrngint

Description: The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025)

Ref Expression
Assertion subrngint ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubRng ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 subrngsubg ⊢ ( 𝑟 ∈ ( SubRng ‘ 𝑅 ) → 𝑟 ∈ ( SubGrp ‘ 𝑅 ) )
2 1 ssriv ⊢ ( SubRng ‘ 𝑅 ) ⊆ ( SubGrp ‘ 𝑅 )
3 sstr ⊢ ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ ( SubRng ‘ 𝑅 ) ⊆ ( SubGrp ‘ 𝑅 ) ) → 𝑆 ⊆ ( SubGrp ‘ 𝑅 ) )
4 2 3 mpan2 ⊢ ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) → 𝑆 ⊆ ( SubGrp ‘ 𝑅 ) )
5 subgint ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
6 4 5 sylan ⊢ ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
7 ssel2 ⊢ ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑟 ∈ 𝑆 ) → 𝑟 ∈ ( SubRng ‘ 𝑅 ) )
8 7 ad4ant14 ⊢ ( ( ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑟 ∈ 𝑆 ) → 𝑟 ∈ ( SubRng ‘ 𝑅 ) )
9 simprl ⊢ ( ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → 𝑥 ∈ ∩ 𝑆 )
10 elinti ⊢ ( 𝑥 ∈ ∩ 𝑆 → ( 𝑟 ∈ 𝑆 → 𝑥 ∈ 𝑟 ) )
11 10 imp ⊢ ( ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑟 ∈ 𝑆 ) → 𝑥 ∈ 𝑟 )
12 9 11 sylan ⊢ ( ( ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑟 ∈ 𝑆 ) → 𝑥 ∈ 𝑟 )
13 simprr ⊢ ( ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → 𝑦 ∈ ∩ 𝑆 )
14 elinti ⊢ ( 𝑦 ∈ ∩ 𝑆 → ( 𝑟 ∈ 𝑆 → 𝑦 ∈ 𝑟 ) )
15 14 imp ⊢ ( ( 𝑦 ∈ ∩ 𝑆 ∧ 𝑟 ∈ 𝑆 ) → 𝑦 ∈ 𝑟 )
16 13 15 sylan ⊢ ( ( ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑟 ∈ 𝑆 ) → 𝑦 ∈ 𝑟 )
17 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
18 17 subrngmcl ⊢ ( ( 𝑟 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑟 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑟 )
19 8 12 16 18 syl3anc ⊢ ( ( ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑟 ∈ 𝑆 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑟 )
20 19 ralrimiva ⊢ ( ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → ∀ 𝑟 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑟 )
21 ovex ⊢ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ V
22 21 elint2 ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 ↔ ∀ 𝑟 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑟 )
23 20 22 sylibr ⊢ ( ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 )
24 23 ralrimivva ⊢ ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∀ 𝑥 ∈ ∩ 𝑆 ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 )
25 ssn0 ⊢ ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ( SubRng ‘ 𝑅 ) ≠ ∅ )
26 n0 ⊢ ( ( SubRng ‘ 𝑅 ) ≠ ∅ ↔ ∃ 𝑟 𝑟 ∈ ( SubRng ‘ 𝑅 ) )
27 subrngrcl ⊢ ( 𝑟 ∈ ( SubRng ‘ 𝑅 ) → 𝑅 ∈ Rng )
28 27 exlimiv ⊢ ( ∃ 𝑟 𝑟 ∈ ( SubRng ‘ 𝑅 ) → 𝑅 ∈ Rng )
29 26 28 sylbi ⊢ ( ( SubRng ‘ 𝑅 ) ≠ ∅ → 𝑅 ∈ Rng )
30 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
31 30 17 issubrng2 ⊢ ( 𝑅 ∈ Rng → ( ∩ 𝑆 ∈ ( SubRng ‘ 𝑅 ) ↔ ( ∩ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ∩ 𝑆 ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 ) ) )
32 25 29 31 3syl ⊢ ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ( ∩ 𝑆 ∈ ( SubRng ‘ 𝑅 ) ↔ ( ∩ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ∩ 𝑆 ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 ) ) )
33 6 24 32 mpbir2and ⊢ ( ( 𝑆 ⊆ ( SubRng ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubRng ‘ 𝑅 ) )