Description: Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lidlincl.1 | ⊢ 𝑈 = ( LIdeal ‘ 𝑅 ) | |
Assertion | lidlincl | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈 ) → ( 𝐼 ∩ 𝐽 ) ∈ 𝑈 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lidlincl.1 | ⊢ 𝑈 = ( LIdeal ‘ 𝑅 ) | |
2 | eqid | ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) | |
3 | 2 1 | lidlacs | ⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( ACS ‘ ( Base ‘ 𝑅 ) ) ) |
4 | 3 | acsmred | ⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( Moore ‘ ( Base ‘ 𝑅 ) ) ) |
5 | mreincl | ⊢ ( ( 𝑈 ∈ ( Moore ‘ ( Base ‘ 𝑅 ) ) ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈 ) → ( 𝐼 ∩ 𝐽 ) ∈ 𝑈 ) | |
6 | 4 5 | syl3an1 | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈 ) → ( 𝐼 ∩ 𝐽 ) ∈ 𝑈 ) |