Metamath Proof Explorer


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 )