This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )