lidlacl

Description: An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lidlcl.u	$⊢ U = LIdeal (R)$
	lidlacl.p	$⊢ \underset{˙}{+} = +_{R}$
Assertion	lidlacl	$⊢ ((R \in Ring \land I \in U) \land (X \in I \land Y \in I)) \to X \underset{˙}{+} Y \in I$

Step	Hyp	Ref	Expression
1		lidlcl.u	$⊢ U = LIdeal (R)$
2		lidlacl.p	$⊢ \underset{˙}{+} = +_{R}$
3		rlmplusg	$⊢ +_{R} = +_{ringLMod (R)}$
4	2 3	eqtri	$⊢ \underset{˙}{+} = +_{ringLMod (R)}$
5	4	oveqi	$⊢ X \underset{˙}{+} Y = X +_{ringLMod (R)} Y$
6		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
7	6	adantr	$⊢ (R \in Ring \land I \in U) \to ringLMod (R) \in LMod$
8		simpr	$⊢ (R \in Ring \land I \in U) \to I \in U$
9		lidlval	$⊢ LIdeal (R) = LSubSp (ringLMod (R))$
10	1 9	eqtri	$⊢ U = LSubSp (ringLMod (R))$
11	8 10	eleqtrdi	$⊢ (R \in Ring \land I \in U) \to I \in LSubSp (ringLMod (R))$
12	7 11	jca	$⊢ (R \in Ring \land I \in U) \to (ringLMod (R) \in LMod \land I \in LSubSp (ringLMod (R)))$
13		eqid	$⊢ +_{ringLMod (R)} = +_{ringLMod (R)}$
14		eqid	$⊢ LSubSp (ringLMod (R)) = LSubSp (ringLMod (R))$
15	13 14	lssvacl	$⊢ ((ringLMod (R) \in LMod \land I \in LSubSp (ringLMod (R))) \land (X \in I \land Y \in I)) \to X +_{ringLMod (R)} Y \in I$
16	12 15	sylan	$⊢ ((R \in Ring \land I \in U) \land (X \in I \land Y \in I)) \to X +_{ringLMod (R)} Y \in I$
17	5 16	eqeltrid	$⊢ ((R \in Ring \land I \in U) \land (X \in I \land Y \in I)) \to X \underset{˙}{+} Y \in I$

Metamath Proof Explorer