Metamath Proof Explorer


Theorem lidlincl

Description: Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024)

Ref Expression
Hypothesis lidlincl.1 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion lidlincl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈𝐽𝑈 ) → ( 𝐼𝐽 ) ∈ 𝑈 )

Proof

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 ∧ 𝐼𝑈𝐽𝑈 ) → ( 𝐼𝐽 ) ∈ 𝑈 )