Metamath Proof Explorer

Theorem lidlincl

Description: Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024)

		Ref	Expression
	Hypothesis	lidlincl.1	$⊢ U = LIdeal (R)$
	Assertion	lidlincl	$⊢ (R \in Ring \land I \in U \land J \in U) \to I \cap J \in U$

Step	Hyp	Ref	Expression
1		lidlincl.1	$⊢ U = LIdeal (R)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	2 1	lidlacs	$⊢ R \in Ring \to U \in ACS ({Base}_{R})$
4	3	acsmred	$⊢ R \in Ring \to U \in Moore ({Base}_{R})$
5		mreincl	$⊢ (U \in Moore ({Base}_{R}) \land I \in U \land J \in U) \to I \cap J \in U$
6	4 5	syl3an1	$⊢ (R \in Ring \land I \in U \land J \in U) \to I \cap J \in U$