Theorem inlidl

Description: The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 28-Jun-2026)

	Ref	Expression
Assertion	inlidl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝐼 ∩ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		intprg	⊢ ( ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → ∩ { 𝐼 , 𝐽 } = ( 𝐼 ∩ 𝐽 ) )
2	1	3adant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → ∩ { 𝐼 , 𝐽 } = ( 𝐼 ∩ 𝐽 ) )
3		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
4		prnzg	⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → { 𝐼 , 𝐽 } ≠ ∅ )
5	4	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → { 𝐼 , 𝐽 } ≠ ∅ )
6		prssi	⊢ ( ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → { 𝐼 , 𝐽 } ⊆ ( LIdeal ‘ 𝑅 ) )
7	6	3adant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → { 𝐼 , 𝐽 } ⊆ ( LIdeal ‘ 𝑅 ) )
8		intlidl	⊢ ( ( 𝑅 ∈ Ring ∧ { 𝐼 , 𝐽 } ≠ ∅ ∧ { 𝐼 , 𝐽 } ⊆ ( LIdeal ‘ 𝑅 ) ) → ∩ { 𝐼 , 𝐽 } ∈ ( LIdeal ‘ 𝑅 ) )
9	3 5 7 8	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → ∩ { 𝐼 , 𝐽 } ∈ ( LIdeal ‘ 𝑅 ) )
10	2 9	eqeltrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐽 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝐼 ∩ 𝐽 ) ∈ ( LIdeal ‘ 𝑅 ) )