lidlnegcl

Description: An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lidlcl.u	$⊢ U = LIdeal (R)$
	lidlnegcl.n	$⊢ N = {inv}_{g} (R)$
Assertion	lidlnegcl	$⊢ (R \in Ring \land I \in U \land X \in I) \to N (X) \in I$

Step	Hyp	Ref	Expression
1		lidlcl.u	$⊢ U = LIdeal (R)$
2		lidlnegcl.n	$⊢ N = {inv}_{g} (R)$
3		rlmvneg	$⊢ {inv}_{g} (R) = {inv}_{g} (ringLMod (R))$
4	2 3	eqtri	$⊢ N = {inv}_{g} (ringLMod (R))$
5	4	fveq1i	$⊢ N (X) = {inv}_{g} (ringLMod (R)) (X)$
6		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
7	6	3ad2ant1	$⊢ (R \in Ring \land I \in U \land X \in I) \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	11	3adant3	$⊢ (R \in Ring \land I \in U \land X \in I) \to I \in LSubSp (ringLMod (R))$
13		simp3	$⊢ (R \in Ring \land I \in U \land X \in I) \to X \in I$
14		eqid	$⊢ LSubSp (ringLMod (R)) = LSubSp (ringLMod (R))$
15		eqid	$⊢ {inv}_{g} (ringLMod (R)) = {inv}_{g} (ringLMod (R))$
16	14 15	lssvnegcl	$⊢ (ringLMod (R) \in LMod \land I \in LSubSp (ringLMod (R)) \land X \in I) \to {inv}_{g} (ringLMod (R)) (X) \in I$
17	7 12 13 16	syl3anc	$⊢ (R \in Ring \land I \in U \land X \in I) \to {inv}_{g} (ringLMod (R)) (X) \in I$
18	5 17	eqeltrid	$⊢ (R \in Ring \land I \in U \land X \in I) \to N (X) \in I$

Metamath Proof Explorer