inidl

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

		Ref	Expression
	Assertion	inidl	$⊢ (R \in RingOps \land I \in Idl (R) \land J \in Idl (R)) \to I \cap J \in Idl (R)$

Step	Hyp	Ref	Expression
1		intprg	$⊢ (I \in Idl (R) \land J \in Idl (R)) \to ⋂ \{I, J\} = I \cap J$
2	1	3adant1	$⊢ (R \in RingOps \land I \in Idl (R) \land J \in Idl (R)) \to ⋂ \{I, J\} = I \cap J$
3		prnzg	$⊢ I \in Idl (R) \to \{I, J\} \neq \emptyset$
4	3	adantr	$⊢ (I \in Idl (R) \land J \in Idl (R)) \to \{I, J\} \neq \emptyset$
5		prssi	$⊢ (I \in Idl (R) \land J \in Idl (R)) \to \{I, J\} \subseteq Idl (R)$
6	4 5	jca	$⊢ (I \in Idl (R) \land J \in Idl (R)) \to (\{I, J\} \neq \emptyset \land \{I, J\} \subseteq Idl (R))$
7		intidl	$⊢ (R \in RingOps \land \{I, J\} \neq \emptyset \land \{I, J\} \subseteq Idl (R)) \to ⋂ \{I, J\} \in Idl (R)$
8	7	3expb	$⊢ (R \in RingOps \land (\{I, J\} \neq \emptyset \land \{I, J\} \subseteq Idl (R))) \to ⋂ \{I, J\} \in Idl (R)$
9	6 8	sylan2	$⊢ (R \in RingOps \land (I \in Idl (R) \land J \in Idl (R))) \to ⋂ \{I, J\} \in Idl (R)$
10	9	3impb	$⊢ (R \in RingOps \land I \in Idl (R) \land J \in Idl (R)) \to ⋂ \{I, J\} \in Idl (R)$
11	2 10	eqeltrrd	$⊢ (R \in RingOps \land I \in Idl (R) \land J \in Idl (R)) \to I \cap J \in Idl (R)$

Metamath Proof Explorer