Metamath Proof Explorer

Theorem intlidl

Description: The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 8-Jun-2024)

Ref Expression
Assertion intlidl ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∩ 𝐶 ∈ ( LIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) )
2 1 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5 3 4 lidlss ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) )
6 2 5 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) )
7 6 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ( Base ‘ 𝑅 ) )
8 pwssb ⊢ ( 𝐶 ⊆ 𝒫 ( Base ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝐶 𝑖 ⊆ ( Base ‘ 𝑅 ) )
9 7 8 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → 𝐶 ⊆ 𝒫 ( Base ‘ 𝑅 ) )
10 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → 𝐶 ≠ ∅ )
11 intss2 ⊢ ( 𝐶 ⊆ 𝒫 ( Base ‘ 𝑅 ) → ( 𝐶 ≠ ∅ → ∩ 𝐶 ⊆ ( Base ‘ 𝑅 ) ) )
12 11 imp ⊢ ( ( 𝐶 ⊆ 𝒫 ( Base ‘ 𝑅 ) ∧ 𝐶 ≠ ∅ ) → ∩ 𝐶 ⊆ ( Base ‘ 𝑅 ) )
13 9 10 12 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∩ 𝐶 ⊆ ( Base ‘ 𝑅 ) )
14 simpl1 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → 𝑅 ∈ Ring )
15 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16 4 15 lidl0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝑖 )
17 14 2 16 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ∈ 𝐶 ) → ( 0g ‘ 𝑅 ) ∈ 𝑖 )
18 17 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝐶 ( 0g ‘ 𝑅 ) ∈ 𝑖 )
19 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
20 19 elint2 ⊢ ( ( 0g ‘ 𝑅 ) ∈ ∩ 𝐶 ↔ ∀ 𝑖 ∈ 𝐶 ( 0g ‘ 𝑅 ) ∈ 𝑖 )
21 18 20 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ ∩ 𝐶 )
22 21 ne0d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∩ 𝐶 ≠ ∅ )
23 14 ad5ant15 ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑅 ∈ Ring )
24 2 ad5ant15 ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
25 simp-4r ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
26 simpllr ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑎 ∈ ∩ 𝐶 )
27 simpr ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑖 ∈ 𝐶 )
28 elinti ⊢ ( 𝑎 ∈ ∩ 𝐶 → ( 𝑖 ∈ 𝐶 → 𝑎 ∈ 𝑖 ) )
29 28 imp ⊢ ( ( 𝑎 ∈ ∩ 𝐶 ∧ 𝑖 ∈ 𝐶 ) → 𝑎 ∈ 𝑖 )
30 26 27 29 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑎 ∈ 𝑖 )
31 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
32 4 3 31 lidlmcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑖 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝑖 )
33 23 24 25 30 32 syl22anc ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝑖 )
34 elinti ⊢ ( 𝑏 ∈ ∩ 𝐶 → ( 𝑖 ∈ 𝐶 → 𝑏 ∈ 𝑖 ) )
35 34 imp ⊢ ( ( 𝑏 ∈ ∩ 𝐶 ∧ 𝑖 ∈ 𝐶 ) → 𝑏 ∈ 𝑖 )
36 35 adantll ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → 𝑏 ∈ 𝑖 )
37 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
38 4 37 lidlacl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝑖 ∧ 𝑏 ∈ 𝑖 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 )
39 23 24 33 36 38 syl22anc ⊢ ( ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) ∧ 𝑖 ∈ 𝐶 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 )
40 39 ralrimiva ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) → ∀ 𝑖 ∈ 𝐶 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 )
41 ovex ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ V
42 41 elint2 ⊢ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ∩ 𝐶 ↔ ∀ 𝑖 ∈ 𝐶 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 )
43 40 42 sylibr ⊢ ( ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) ∧ 𝑏 ∈ ∩ 𝐶 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ∩ 𝐶 )
44 43 ralrimiva ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑎 ∈ ∩ 𝐶 ) → ∀ 𝑏 ∈ ∩ 𝐶 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ∩ 𝐶 )
45 44 anasss ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ ∩ 𝐶 ) ) → ∀ 𝑏 ∈ ∩ 𝐶 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ∩ 𝐶 )
46 45 ralrimivva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ ∩ 𝐶 ∀ 𝑏 ∈ ∩ 𝐶 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ∩ 𝐶 )
47 4 3 37 31 islidl ⊢ ( ∩ 𝐶 ∈ ( LIdeal ‘ 𝑅 ) ↔ ( ∩ 𝐶 ⊆ ( Base ‘ 𝑅 ) ∧ ∩ 𝐶 ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑎 ∈ ∩ 𝐶 ∀ 𝑏 ∈ ∩ 𝐶 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ∩ 𝐶 ) )
48 13 22 46 47 syl3anbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∩ 𝐶 ∈ ( LIdeal ‘ 𝑅 ) )