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

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

Proof

Step Hyp Ref Expression
1 subrgsubg ⊢ ( 𝑟 ∈ ( SubRing ‘ 𝑅 ) → 𝑟 ∈ ( SubGrp ‘ 𝑅 ) )
2 1 ssriv ⊢ ( SubRing ‘ 𝑅 ) ⊆ ( SubGrp ‘ 𝑅 )
3 sstr ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ ( SubRing ‘ 𝑅 ) ⊆ ( SubGrp ‘ 𝑅 ) ) → 𝑆 ⊆ ( SubGrp ‘ 𝑅 ) )
4 2 3 mpan2 ⊢ ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ ( SubGrp ‘ 𝑅 ) )
5 subgint ⊢ ( ( 𝑆 ⊆ ( SubGrp ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
6 4 5 sylan ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
7 ssel2 ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑟 ∈ 𝑆 ) → 𝑟 ∈ ( SubRing ‘ 𝑅 ) )
8 7 adantlr ⊢ ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝑆 ) → 𝑟 ∈ ( SubRing ‘ 𝑅 ) )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 9 subrg1cl ⊢ ( 𝑟 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑟 )
11 8 10 syl ⊢ ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝑆 ) → ( 1r ‘ 𝑅 ) ∈ 𝑟 )
12 11 ralrimiva ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∀ 𝑟 ∈ 𝑆 ( 1r ‘ 𝑅 ) ∈ 𝑟 )
13 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
14 13 elint2 ⊢ ( ( 1r ‘ 𝑅 ) ∈ ∩ 𝑆 ↔ ∀ 𝑟 ∈ 𝑆 ( 1r ‘ 𝑅 ) ∈ 𝑟 )
15 12 14 sylibr ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ( 1r ‘ 𝑅 ) ∈ ∩ 𝑆 )
16 8 adantlr ⊢ ( ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑟 ∈ 𝑆 ) → 𝑟 ∈ ( SubRing ‘ 𝑅 ) )
17 simprl ⊢ ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → 𝑥 ∈ ∩ 𝑆 )
18 elinti ⊢ ( 𝑥 ∈ ∩ 𝑆 → ( 𝑟 ∈ 𝑆 → 𝑥 ∈ 𝑟 ) )
19 18 imp ⊢ ( ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑟 ∈ 𝑆 ) → 𝑥 ∈ 𝑟 )
20 17 19 sylan ⊢ ( ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑟 ∈ 𝑆 ) → 𝑥 ∈ 𝑟 )
21 simprr ⊢ ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → 𝑦 ∈ ∩ 𝑆 )
22 elinti ⊢ ( 𝑦 ∈ ∩ 𝑆 → ( 𝑟 ∈ 𝑆 → 𝑦 ∈ 𝑟 ) )
23 22 imp ⊢ ( ( 𝑦 ∈ ∩ 𝑆 ∧ 𝑟 ∈ 𝑆 ) → 𝑦 ∈ 𝑟 )
24 21 23 sylan ⊢ ( ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑟 ∈ 𝑆 ) → 𝑦 ∈ 𝑟 )
25 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26 25 subrgmcl ⊢ ( ( 𝑟 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑟 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑟 )
27 16 20 24 26 syl3anc ⊢ ( ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) ∧ 𝑟 ∈ 𝑆 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑟 )
28 27 ralrimiva ⊢ ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → ∀ 𝑟 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑟 )
29 ovex ⊢ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ V
30 29 elint2 ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 ↔ ∀ 𝑟 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑟 )
31 28 30 sylibr ⊢ ( ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) ∧ ( 𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 )
32 31 ralrimivva ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∀ 𝑥 ∈ ∩ 𝑆 ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 )
33 ssn0 ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ( SubRing ‘ 𝑅 ) ≠ ∅ )
34 n0 ⊢ ( ( SubRing ‘ 𝑅 ) ≠ ∅ ↔ ∃ 𝑟 𝑟 ∈ ( SubRing ‘ 𝑅 ) )
35 subrgrcl ⊢ ( 𝑟 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
36 35 exlimiv ⊢ ( ∃ 𝑟 𝑟 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
37 34 36 sylbi ⊢ ( ( SubRing ‘ 𝑅 ) ≠ ∅ → 𝑅 ∈ Ring )
38 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
39 38 9 25 issubrg2 ⊢ ( 𝑅 ∈ Ring → ( ∩ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ∩ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ ∩ 𝑆 ∧ ∀ 𝑥 ∈ ∩ 𝑆 ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 ) ) )
40 33 37 39 3syl ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ( ∩ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ∩ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ ∩ 𝑆 ∧ ∀ 𝑥 ∈ ∩ 𝑆 ∀ 𝑦 ∈ ∩ 𝑆 ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ∩ 𝑆 ) ) )
41 6 15 32 40 mpbir3and ⊢ ( ( 𝑆 ⊆ ( SubRing ‘ 𝑅 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ( SubRing ‘ 𝑅 ) )