Metamath Proof Explorer

Theorem inidl

Description: Obsolete theorem, use inlidl instead. The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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)$