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