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	$⊢ (R \in Ring \land I \in LIdeal (R) \land J \in LIdeal (R)) \to I \cap J \in LIdeal (R)$

Step	Hyp	Ref	Expression
1		intprg	$⊢ (I \in LIdeal (R) \land J \in LIdeal (R)) \to ⋂ \{I, J\} = I \cap J$
2	1	3adant1	$⊢ (R \in Ring \land I \in LIdeal (R) \land J \in LIdeal (R)) \to ⋂ \{I, J\} = I \cap J$
3		simp1	$⊢ (R \in Ring \land I \in LIdeal (R) \land J \in LIdeal (R)) \to R \in Ring$
4		prnzg	$⊢ I \in LIdeal (R) \to \{I, J\} \neq \emptyset$
5	4	3ad2ant2	$⊢ (R \in Ring \land I \in LIdeal (R) \land J \in LIdeal (R)) \to \{I, J\} \neq \emptyset$
6		prssi	$⊢ (I \in LIdeal (R) \land J \in LIdeal (R)) \to \{I, J\} \subseteq LIdeal (R)$
7	6	3adant1	$⊢ (R \in Ring \land I \in LIdeal (R) \land J \in LIdeal (R)) \to \{I, J\} \subseteq LIdeal (R)$
8		intlidl	$⊢ (R \in Ring \land \{I, J\} \neq \emptyset \land \{I, J\} \subseteq LIdeal (R)) \to ⋂ \{I, J\} \in LIdeal (R)$
9	3 5 7 8	syl3anc	$⊢ (R \in Ring \land I \in LIdeal (R) \land J \in LIdeal (R)) \to ⋂ \{I, J\} \in LIdeal (R)$
10	2 9	eqeltrrd	$⊢ (R \in Ring \land I \in LIdeal (R) \land J \in LIdeal (R)) \to I \cap J \in LIdeal (R)$

Metamath Proof Explorer