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