Theorem 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 = ( invg ` R )
Assertion	lidlnegcl	|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( N ` X ) e. I )

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	|- U = ( LIdeal ` R )
2		lidlnegcl.n	|- N = ( invg ` R )
3		rlmvneg	|- ( invg ` R ) = ( invg ` ( ringLMod ` R ) )
4	2 3	eqtri	|- N = ( invg ` ( ringLMod ` R ) )
5	4	fveq1i	|- ( N ` X ) = ( ( invg ` ( ringLMod ` R ) ) ` X )
6		rlmlmod	|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )
7	6	3ad2ant1	|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( ringLMod ` R ) e. LMod )
8		simpr	|- ( ( R e. Ring /\ I e. U ) -> I e. U )
9		lidlval	|- ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) )
10	1 9	eqtri	|- U = ( LSubSp ` ( ringLMod ` R ) )
11	8 10	eleqtrdi	|- ( ( R e. Ring /\ I e. U ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) )
12	11	3adant3	|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) )
13		simp3	|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> X e. I )
14		eqid	|- ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) )
15		eqid	|- ( invg ` ( ringLMod ` R ) ) = ( invg ` ( ringLMod ` R ) )
16	14 15	lssvnegcl	|- ( ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) /\ X e. I ) -> ( ( invg ` ( ringLMod ` R ) ) ` X ) e. I )
17	7 12 13 16	syl3anc	|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( ( invg ` ( ringLMod ` R ) ) ` X ) e. I )
18	5 17	eqeltrid	|- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( N ` X ) e. I )